Theorem re1luk3
luk-3 derived from the Tarski-Bernays-Wajsberg axioms.
This theorem, along with re1luk1 and re1luk2 proves that tbw-ax1,
tbw-ax2, tbw-ax3, and tbw-ax4, with [ax-mp] can be used as a
complete axiom system for all of propositional calculus. (Contributed by
Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \varphi \rightarrow \neg \varphi \rightarrow \psi \)
Proof
l0
tbw-ax4
\( \vdash \bot \rightarrow \psi \)
l1
tbw-ax1
\( \vdash (\varphi \rightarrow \bot) \rightarrow (\bot \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
tbwlem1
\( \vdash ((\varphi \rightarrow \bot) \rightarrow (\bot \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\bot \rightarrow \psi) \rightarrow (\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \)
ax-mp l1 _
\( \vdash (\bot \rightarrow \psi) \rightarrow (\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \)
l4
ax-mp l0 _
\( \vdash (\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi \)
tbwlem1
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow (\varphi \rightarrow \bot) \rightarrow \psi \)
l6
ax-mp l4 _
\( \vdash \varphi \rightarrow (\varphi \rightarrow \bot) \rightarrow \psi \)
l7
tbw-negdf
\( \vdash ((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot \)
tbwlem5
\( \vdash (((\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \neg \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow \neg \varphi \rightarrow \varphi \rightarrow \bot \)
l9
ax-mp l7 _
\( \vdash \neg \varphi \rightarrow \varphi \rightarrow \bot \)
tbw-ax1
\( \vdash (\neg \varphi \rightarrow \varphi \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \psi \)
ax-mp l9 _
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow \neg \varphi \rightarrow \psi \)
tbwsyl l6 _