Theorem tarski-bernays-ax2
Derivation of [ax-2] from the Tarski-Bernays axiom set { [ax-1],
imim1, peirce }. Note that no inference rule other than [ax-mp] is
used in this proof. This proof establishes a circle of equivalence: From
{ impsingle }, { [ax-1], imim1, peirce } was proved. From {
[ax-1], imim1, peirce }, { [ax-1], [ax-2] and peirce } was
proved. From { [ax-1], [ax-2] and peirce }, { impsingle } was
proved. Therefore, the theorems that can be proved by selecting any one
of these three distinct axiom sets must be equivalent. Prover9 and mmj2
were used to help constuct this proof. (Contributed by Larry Lesyna and
Jeffrey P. Machado, 1-Aug-2023.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
peirce
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-1
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l2
ax-mp l0 _
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l4
ax-mp l2 _
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l5
peirce
\( \vdash ((((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l6
imim1
\( \vdash ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l6 _
\( \vdash (((((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l5 _
\( \vdash ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l10
ax-mp l4 _
\( \vdash (((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l11
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l11 _
\( \vdash ((((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l14
ax-mp l10 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l15
imim1
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l15 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l18
ax-mp l14 _
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l19
imim1
\( \vdash ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
imim1
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l19 _
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l22
ax-mp l18 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l23
peirce
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l24
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l24 _
\( \vdash ((((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l27
ax-mp l23 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l28
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l28 _
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l31
ax-mp l27 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l32
ax-1
\( \vdash (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l32 _
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l35
ax-mp l31 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l36
imim1
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l38
ax-mp l36 _
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l39
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l39 _
\( \vdash ((((((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l38 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l35 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l44
ax-mp l22 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l45
imim1
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l45 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l48
ax-mp l44 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l49
peirce
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l50
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l50 _
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l53
ax-mp l49 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l54
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l54 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l57
ax-mp l53 _
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l58
ax-1
\( \vdash ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l58 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l61
ax-mp l57 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l62
imim1
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l64
ax-mp l62 _
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l65
imim1
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l65 _
\( \vdash (((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l64 _
\( \vdash (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l61 _
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l70
ax-mp l48 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l71
imim1
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \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 \)
ax-mp l71 _
\( \vdash (((\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 \)
l74
ax-mp l70 _
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l75
peirce
\( \vdash (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l76
imim1
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l76 _
\( \vdash ((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l79
ax-mp l75 _
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l80
imim1
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l80 _
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l83
ax-mp l79 _
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l84
ax-1
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi \)
imim1
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l84 _
\( \vdash ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l87
ax-mp l83 _
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l88
imim1
\( \vdash ((\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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((\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 \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \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 \psi) \rightarrow \varphi \rightarrow \chi \)
l90
ax-mp l88 _
\( \vdash (((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \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 \psi) \rightarrow \varphi \rightarrow \chi \)
l91
imim1
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
imim1
\( \vdash (((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \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 \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \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 \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l91 _
\( \vdash ((((((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \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 \psi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \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 \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l90 _
\( \vdash ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \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 \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l87 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l74 _