Theorem tarski-bernays-ax2 1643

Description: Derivation of ax-2 7 from the Tarski-Bernays axiom set { ax-1 6, imim1 83, peirce 201 }. Note that no inference rule other than ax-mp 5 is used in this proof. This proof establishes a circle of equivalence: From { impsingle 1630 }, { ax-1 6, imim1 83, peirce 201 } was proved. From { ax-1 6, imim1 83, peirce 201 }, { ax-1 6, ax-2 7 and peirce 201 } was proved. From { ax-1 6, ax-2 7 and peirce 201 }, { impsingle 1630 } 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.)

Assertion

Ref	Expression
tarski-bernays-ax2	⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Proof of Theorem tarski-bernays-ax2

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by: (None)