Theorem mercolem6
Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2.
(Contributed by Anthony Hart, 16-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
Proof
l0
merco2
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
l1
mercolem1
\( \vdash ((\varphi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
mercolem1
\( \vdash (((\varphi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l3
ax-mp l1 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l4
mercolem5
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
mercolem4
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l4 _
\( \vdash ((\varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l3 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l8
ax-mp l0 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l9
mercolem1
\( \vdash ((\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
mercolem1
\( \vdash (((\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l11
ax-mp l9 _
\( \vdash ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l12
mercolem5
\( \vdash (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
mercolem4
\( \vdash ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l12 _
\( \vdash (((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l11 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _
\( \vdash ((\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l8 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \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 \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _