Theorem minimp-syllsimp
Derivation of Syll-Simp ( jarr) 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 \chi) \rightarrow \psi \rightarrow \chi \)
Proof
l0
minimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
l1
minimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \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 \chi) \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 \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi \)
l3
ax-mp l1 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \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 \chi) \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 \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi \)
l4
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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi \)
l5
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 \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \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 \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \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 \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \)
mp2 l4 l5 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \)
l8
mp2b l0 l3 _
\( \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \)
l9
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 \)
l10
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 \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
l11
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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \)
l12
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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
mp2 l11 l12 _
\( \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \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 \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
l15
mp2b l9 l10 _
\( \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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
l16
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 \)
l17
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 \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\psi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
l18
minimp
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi \)
l19
minimp
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
minimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\psi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
mp2 l18 l19 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\psi \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
mp2b l16 l17 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)
mp2b l8 l15 _