Theorem re2luk2
luk-2 derived from Russell-Bernays'. (Contributed by Anthony Hart,
19-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
rb-ax4
\( \vdash \neg (\varphi \vee \varphi) \vee \varphi \)
rb-ax3
\( \vdash \neg \varphi \vee (\varphi \vee \varphi) \)
l2
rbsyl l0 _
\( \vdash \neg \varphi \vee \varphi \)
l3
rb-ax4
\( \vdash \neg (\neg \neg \varphi \vee \neg \neg \varphi) \vee \neg \neg \varphi \)
rb-ax3
\( \vdash \neg \neg \neg \varphi \vee (\neg \neg \varphi \vee \neg \neg \varphi) \)
l5
rbsyl l3 _
\( \vdash \neg \neg \neg \varphi \vee \neg \neg \varphi \)
rb-ax2
\( \vdash \neg (\neg \neg \neg \varphi \vee \neg \neg \varphi) \vee (\neg \neg \varphi \vee \neg \neg \neg \varphi) \)
anmp l5 _
rblem1 _ l2
\( \vdash \neg (\neg \varphi \vee \varphi) \vee (\neg \neg \neg \varphi \vee \varphi) \)
anmp l2 _
rblem1 _ l2
\( \vdash \neg (\neg \neg \varphi \vee \varphi) \vee (\varphi \vee \varphi) \)
l11
rbsyl l0 _
\( \vdash \neg (\neg \neg \varphi \vee \varphi) \vee \varphi \)
rb-imdf
rblem6 _
\( \vdash \neg (\neg \varphi \rightarrow \varphi) \vee (\neg \neg \varphi \vee \varphi) \)
l14
rbsyl l11 _
\( \vdash \neg (\neg \varphi \rightarrow \varphi) \vee \varphi \)
rb-imdf
rblem7 _
\( \vdash \neg (\neg (\neg \varphi \rightarrow \varphi) \vee \varphi) \vee ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \)
anmp l14 _