Theorem retbwax2
tbw-ax2 rederived from merco1. (Contributed by Anthony Hart,
17-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \)
Proof
l0
merco1lem1
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
merco1
\( \vdash (((((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l2
ax-mp l0 _
\( \vdash ((\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l3
merco1
\( \vdash ((((\varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \bot) \rightarrow \bot) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
merco1
\( \vdash (((((\varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi \rightarrow \bot) \rightarrow \bot) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
ax-mp l3 _
\( \vdash (((\bot \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l6
ax-mp l2 _
\( \vdash \varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l7
merco1lem1
\( \vdash ((((\psi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
merco1
\( \vdash (((((\psi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
l9
ax-mp l7 _
\( \vdash ((\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
l10
merco1
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \varphi) \rightarrow \psi \rightarrow \bot) \rightarrow (\varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow (\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
merco1
\( \vdash (((((\varphi \rightarrow \psi \rightarrow \varphi) \rightarrow \psi \rightarrow \bot) \rightarrow (\varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot) \rightarrow (\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow (((\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l10 _
\( \vdash (((\bot \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l9 _
\( \vdash (\varphi \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l6 _