Theorem minimp-ax2c
Derivation of a commuted form of [ax-2] from [ax-mp] and minimp.
(Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
minimp
\( \vdash \varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
minimp
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l2
ax-mp l0 _
\( \vdash (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l3
minimp
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi \)
l4
minimp
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \)
l5
minimp
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l6
minimp
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l7
minimp
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
minimp
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \)
l9
mp2 l6 l7 _
\( \vdash ((\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \)
minimp
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \)
ax-mp l4 _
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \)
l12
mp2 l5 l9 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \)
minimp
\( \vdash ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l14
mp2 l4 l12 _
\( \vdash (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
minimp-syllsimp
\( \vdash ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
l16
ax-mp l14 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \)
minimp
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l18
mp2 l3 l16 _
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
minimp-syllsimp
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l20
ax-mp l18 _
\( \vdash (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l21
minimp
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l22
minimp
\( \vdash (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
minimp
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l24
ax-mp l22 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
minimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l26
mp2 l21 l24 _
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l27
minimp-syllsimp
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
minimp-syllsimp
\( \vdash (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mp2 l26 l27 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mp2 l2 l20 _