Theorem re2luk1
luk-1 derived from Russell-Bernays'. (Contributed by Anthony Hart,
19-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
rb-imdf
l1
rblem7 _
\( \vdash \neg (\neg (\psi \rightarrow \chi) \vee (\varphi \rightarrow \chi)) \vee ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \)
rb-imdf
l3
rblem6 _
\( \vdash \neg (\psi \rightarrow \chi) \vee (\neg \psi \vee \chi) \)
l4
rb-ax2
\( \vdash \neg (\neg (\psi \rightarrow \chi) \vee \neg \neg (\neg \psi \vee \chi)) \vee (\neg \neg (\neg \psi \vee \chi) \vee \neg (\psi \rightarrow \chi)) \)
l5
rb-ax4
\( \vdash \neg (\neg (\psi \rightarrow \chi) \vee \neg (\psi \rightarrow \chi)) \vee \neg (\psi \rightarrow \chi) \)
rb-ax3
\( \vdash \neg \neg (\psi \rightarrow \chi) \vee (\neg (\psi \rightarrow \chi) \vee \neg (\psi \rightarrow \chi)) \)
l7
rbsyl l5 _
l8
rb-ax4
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee \neg (\neg \psi \vee \chi)) \vee \neg (\neg \psi \vee \chi) \)
rb-ax3
\( \vdash \neg \neg (\neg \psi \vee \chi) \vee (\neg (\neg \psi \vee \chi) \vee \neg (\neg \psi \vee \chi)) \)
l10
rbsyl l8 _
\( \vdash \neg \neg (\neg \psi \vee \chi) \vee \neg (\neg \psi \vee \chi) \)
rb-ax2
\( \vdash \neg (\neg \neg (\neg \psi \vee \chi) \vee \neg (\neg \psi \vee \chi)) \vee (\neg (\neg \psi \vee \chi) \vee \neg \neg (\neg \psi \vee \chi)) \)
anmp l10 _
rblem1 l7 _
\( \vdash \neg (\neg (\psi \rightarrow \chi) \vee (\neg \psi \vee \chi)) \vee (\neg (\psi \rightarrow \chi) \vee \neg \neg (\neg \psi \vee \chi)) \)
rbsyl l4 _
\( \vdash \neg (\neg (\psi \rightarrow \chi) \vee (\neg \psi \vee \chi)) \vee (\neg \neg (\neg \psi \vee \chi) \vee \neg (\psi \rightarrow \chi)) \)
l15
anmp l3 _
rb-imdf
rblem7 _
l18
rblem1 l15 _
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi)) \vee (\neg (\psi \rightarrow \chi) \vee (\varphi \rightarrow \chi)) \)
l19
rb-ax1
\( \vdash \neg (\neg \psi \vee \chi) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi)) \)
l20
rb-ax2
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi) \vee \neg (\neg \varphi \vee \psi)) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi))) \)
l21
rb-ax4
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi)) \vee \neg (\neg \varphi \vee \psi) \)
rb-ax3
\( \vdash \neg \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi)) \)
l23
rbsyl l21 _
l24
rb-ax4
\( \vdash \neg (\neg \varphi \vee \chi \vee (\neg \varphi \vee \chi)) \vee (\neg \varphi \vee \chi) \)
rb-ax3
\( \vdash \neg (\neg \varphi \vee \chi) \vee (\neg \varphi \vee \chi \vee (\neg \varphi \vee \chi)) \)
rbsyl l24 _
l27
rblem4 l23 _ l10
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi) \vee \neg (\neg \psi \vee \chi)) \vee (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi) \vee \neg (\neg \varphi \vee \psi)) \)
rb-ax2
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi))) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi) \vee \neg (\neg \psi \vee \chi)) \)
rbsyl l27 _
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi))) \vee (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi) \vee \neg (\neg \varphi \vee \psi)) \)
rbsyl l20 _
\( \vdash \neg (\neg (\neg \psi \vee \chi) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg \varphi \vee \chi))) \vee (\neg (\neg \varphi \vee \psi) \vee (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi))) \)
anmp l19 _
\( \vdash \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \psi \vee \chi) \vee (\neg \varphi \vee \chi)) \)
l32
rbsyl l18 _
\( \vdash \neg (\neg \varphi \vee \psi) \vee (\neg (\psi \rightarrow \chi) \vee (\varphi \rightarrow \chi)) \)
rb-imdf
rblem6 _
\( \vdash \neg (\varphi \rightarrow \psi) \vee (\neg \varphi \vee \psi) \)
rbsyl l32 _
\( \vdash \neg (\varphi \rightarrow \psi) \vee (\neg (\psi \rightarrow \chi) \vee (\varphi \rightarrow \chi)) \)
l36
rbsyl l1 _
\( \vdash \neg (\varphi \rightarrow \psi) \vee ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \)
rb-imdf
rblem7 _
\( \vdash \neg (\neg (\varphi \rightarrow \psi) \vee ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi)) \vee ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \)
anmp l36 _