tarski-bernays-ax2

Description: 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.)

		Ref	Expression
	Assertion	tarski-bernays-ax2	$⊢ (φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		peirce	$⊢ (((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)$
2		ax-1	$⊢ ((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
3	1 2	ax-mp	$⊢ (((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))$
4		imim1	$⊢ ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
5	3 4	ax-mp	$⊢ (((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
6		peirce	$⊢ ((((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
7		imim1	$⊢ ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
8		imim1	$⊢ (((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))) \to ((((((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))))$
9	7 8	ax-mp	$⊢ (((((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
10	6 9	ax-mp	$⊢ ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
11	5 10	ax-mp	$⊢ (((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))$
12		imim1	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to (((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
13		imim1	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to (((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
14	12 13	ax-mp	$⊢ ((((((φ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
15	11 14	ax-mp	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))$
16		imim1	$⊢ (((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ)))$
17		imim1	$⊢ ((((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ)))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
18	16 17	ax-mp	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
19	15 18	ax-mp	$⊢ (((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))$
20		imim1	$⊢ ((ψ \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to ((ψ \to χ) \to χ))$
21		imim1	$⊢ (((ψ \to χ) \to (φ \to χ)) \to (((φ \to χ) \to χ) \to ((ψ \to χ) \to χ))) \to (((((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))))$
22	20 21	ax-mp	$⊢ ((((φ \to χ) \to χ) \to ((ψ \to χ) \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)))$
23	19 22	ax-mp	$⊢ ((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))$
24		peirce	$⊢ (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
25		imim1	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
26		imim1	$⊢ ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
27	25 26	ax-mp	$⊢ ((((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
28	24 27	ax-mp	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
29		imim1	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
30		imim1	$⊢ ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
31	29 30	ax-mp	$⊢ ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
32	28 31	ax-mp	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
33		ax-1	$⊢ (((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ)))$
34		imim1	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ)))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
35	33 34	ax-mp	$⊢ ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
36	32 35	ax-mp	$⊢ (((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
37		imim1	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))$
38		imim1	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))))$
39	37 38	ax-mp	$⊢ (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))$
40		imim1	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))$
41		imim1	$⊢ (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))) \to (((((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))))$
42	40 41	ax-mp	$⊢ ((((((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))))$
43	39 42	ax-mp	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))$
44	36 43	ax-mp	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))$
45	23 44	ax-mp	$⊢ (((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))$
46		imim1	$⊢ (φ \to (ψ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))$
47		imim1	$⊢ ((φ \to (ψ \to χ)) \to (((ψ \to χ) \to χ) \to (φ \to χ))) \to (((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))))$
48	46 47	ax-mp	$⊢ ((((ψ \to χ) \to χ) \to (φ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)))$
49	45 48	ax-mp	$⊢ (φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))$
50		peirce	$⊢ ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
51		imim1	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
52		imim1	$⊢ (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
53	51 52	ax-mp	$⊢ (((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
54	50 53	ax-mp	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
55		imim1	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
56		imim1	$⊢ (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
57	55 56	ax-mp	$⊢ (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
58	54 57	ax-mp	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
59		ax-1	$⊢ ((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ)))$
60		imim1	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ)))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
61	59 60	ax-mp	$⊢ (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
62	58 61	ax-mp	$⊢ ((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
63		imim1	$⊢ ((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))$
64		imim1	$⊢ (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))$
65	63 64	ax-mp	$⊢ ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))$
66		imim1	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))$
67		imim1	$⊢ ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))) \to ((((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))))$
68	66 67	ax-mp	$⊢ (((((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))$
69	65 68	ax-mp	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((((ψ \to χ) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))$
70	62 69	ax-mp	$⊢ ((φ \to (ψ \to χ)) \to (((ψ \to χ) \to (φ \to χ)) \to (φ \to χ))) \to (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))$
71	49 70	ax-mp	$⊢ ((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$
72		imim1	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$
73		imim1	$⊢ ((φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))) \to ((((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))$
74	72 73	ax-mp	$⊢ (((ψ \to χ) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))$
75	71 74	ax-mp	$⊢ (φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$
76		peirce	$⊢ (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
77		imim1	$⊢ (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
78		imim1	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to (((((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
79	77 78	ax-mp	$⊢ ((((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
80	76 79	ax-mp	$⊢ (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
81		imim1	$⊢ (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
82		imim1	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
83	81 82	ax-mp	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
84	80 83	ax-mp	$⊢ (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
85		ax-1	$⊢ (φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ)))$
86		imim1	$⊢ ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ)))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))))$
87	85 86	ax-mp	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)))$
88	84 87	ax-mp	$⊢ (φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))$
89		imim1	$⊢ ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))$
90		imim1	$⊢ (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))) \to ((((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))))$
91	89 90	ax-mp	$⊢ (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))$
92		imim1	$⊢ ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))$
93		imim1	$⊢ (((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))) \to (((((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))) \to (((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))))$
94	92 93	ax-mp	$⊢ ((((((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))) \to (((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))))$
95	91 94	ax-mp	$⊢ ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to χ)) \to (φ \to χ))) \to (((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))))$
96	88 95	ax-mp	$⊢ ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ)))$
97	75 96	ax-mp	$⊢ (φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$

Metamath Proof Explorer

Theorem tarski-bernays-ax2

Proof