Theorem re2luk3
luk-3 derived from Russell-Bernays'.
This theorem, along with re1axmp, re2luk1, and re2luk2 shows that
rb-ax1, rb-ax2, rb-ax3, and rb-ax4, along with anmp, can be
used as a complete axiomatization of propositional calculus. (Contributed
by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \varphi \rightarrow \neg \varphi \rightarrow \psi \)
Proof
rb-imdf
l1
rblem7 _
\( \vdash \neg (\neg \neg \varphi \vee \psi) \vee (\neg \varphi \rightarrow \psi) \)
l2
rb-ax4
\( \vdash \neg (\neg \varphi \vee \neg \varphi) \vee \neg \varphi \)
rb-ax3
\( \vdash \neg \neg \varphi \vee (\neg \varphi \vee \neg \varphi) \)
l4
rbsyl l2 _
\( \vdash \neg \neg \varphi \vee \neg \varphi \)
rb-ax2
\( \vdash \neg (\neg \neg \varphi \vee \neg \varphi) \vee (\neg \varphi \vee \neg \neg \varphi) \)
l6
anmp l4 _
\( \vdash \neg \varphi \vee \neg \neg \varphi \)
rblem2
\( \vdash \neg (\neg \varphi \vee \neg \neg \varphi) \vee (\neg \varphi \vee (\neg \neg \varphi \vee \psi)) \)
anmp l6 _
\( \vdash \neg \varphi \vee (\neg \neg \varphi \vee \psi) \)
l9
rbsyl l1 _
\( \vdash \neg \varphi \vee (\neg \varphi \rightarrow \psi) \)
rb-imdf
rblem7 _
\( \vdash \neg (\neg \varphi \vee (\neg \varphi \rightarrow \psi)) \vee (\varphi \rightarrow \neg \varphi \rightarrow \psi) \)
anmp l9 _