Theorem retbwax1
tbw-ax1 rederived from merco1.
This theorem, along with retbwax2, retbwax3, and retbwax4, shows
that merco1 with [ax-mp] can be used as a complete axiomatization of
propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
merco1lem18
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
merco1lem16
\( \vdash ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
l2
ax-mp l0 _
\( \vdash (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
l3
merco1lem15
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem15
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l5
ax-mp l3 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem18
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l7
ax-mp l5 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem14
\( \vdash ((((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l9
ax-mp l7 _
\( \vdash (\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l10
merco1lem14
\( \vdash ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l11
merco1lem10
\( \vdash ((((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot \)
merco1
\( \vdash (((((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot \)
l13
ax-mp l11 _
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot \)
merco1
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l15
ax-mp l13 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow \bot) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l15 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l18
ax-mp l10 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem15
\( \vdash (((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l20
ax-mp l18 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l21
merco1lem10
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem9
\( \vdash ((((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l23
ax-mp l21 _
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
merco1lem13
\( \vdash ((((((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l23 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \bot) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l20 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l9 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l2 _