Theorem minimp-ax2c 1554

Description: Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1551. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
minimp-ax2c	⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))

Proof of Theorem minimp-ax2c

Step	Hyp	Ref	Expression
1		minimp 1551	. . 3 ⊢ (𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))
2		minimp 1551	. . 3 ⊢ ((𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
4		minimp 1551	. . . 4 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → ((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))))))
5		minimp 1551	. . . . . 6 ⊢ ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)))))
6		minimp 1551	. . . . . . 7 ⊢ ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))
7		minimp 1551	. . . . . . . 8 ⊢ (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))))))
8		minimp 1551	. . . . . . . 8 ⊢ (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))
9		minimp 1551	. . . . . . . 8 ⊢ ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))))))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))))
10	7, 8, 9	mp2 9	. . . . . . 7 ⊢ (((𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))
11		minimp 1551	. . . . . . . 8 ⊢ (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → ((((𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → 𝜑))))
12	5, 11	ax-mp 5	. . . . . . 7 ⊢ (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → ((((𝜑 → ((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑)))) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → 𝜑)))
13	6, 10, 12	mp2 9	. . . . . 6 ⊢ ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → 𝜑)
14		minimp 1551	. . . . . 6 ⊢ (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑))))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → 𝜑) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (𝜑 → (𝜓 → 𝜒))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)))))
15	5, 13, 14	mp2 9	. . . . 5 ⊢ ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (𝜑 → (𝜓 → 𝜒))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)))
16		minimp-sylsimp 1552	. . . . 5 ⊢ (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑)) → (𝜑 → (𝜓 → 𝜒))) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒))))
17	15, 16	ax-mp 5	. . . 4 ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)))
18		minimp 1551	. . . 4 ⊢ (((𝜑 → (𝜓 → 𝜒)) → (((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → ((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒)))))) → (((𝜑 → (𝜓 → 𝜒)) → ((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒))) → ((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))
19	4, 17, 18	mp2 9	. . 3 ⊢ ((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
20		minimp-sylsimp 1552	. . 3 ⊢ (((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))
21	19, 20	ax-mp 5	. 2 ⊢ ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
22		minimp 1551	. . . 4 ⊢ (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))))
23		minimp 1551	. . . . 5 ⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓)))))
24		minimp 1551	. . . . 5 ⊢ (((𝜑 → 𝜓) → (((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → (𝜑 → 𝜓))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))))
25	23, 24	ax-mp 5	. . . 4 ⊢ (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))
26		minimp 1551	. . . 4 ⊢ ((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))))) → ((((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))) → (((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))))))
27	22, 25, 26	mp2 9	. . 3 ⊢ (((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))))
28		minimp-sylsimp 1552	. . 3 ⊢ (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))
29		minimp-sylsimp 1552	. . 3 ⊢ ((((((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))) → ((((((𝜑 → 𝜓) → (𝜑 → 𝜓)) → ((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))))) → (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))))
30	27, 28, 29	mp2 9	. 2 ⊢ (((𝜑 → 𝜓) → (((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → (((((((𝜑 → 𝜑) → (((𝜑 → 𝜑) → (𝜑 → 𝜑)) → (𝜑 → 𝜑))) → 𝜑) → (𝜓 → 𝜒)) → (𝜑 → 𝜒)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) → ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))))
31	3, 21, 30	mp2 9	1 ⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))

Syntax hints:   → wi 4

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

This theorem is referenced by:  minimp-ax2  1555