minimp-ax2c

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

		Ref	Expression
	Assertion	minimp-ax2c	$⊢ (φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		minimp	$⊢ φ \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))$
2		minimp	$⊢ (φ \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 χ))$
4		minimp	$⊢ (φ \to (ψ \to χ)) \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		minimp	$⊢ (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \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		minimp	$⊢ (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))$
7		minimp	$⊢ ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \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		minimp	$⊢ ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))$
9		minimp	$⊢ (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))))) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))))))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((φ \to ((φ \to φ) \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	7 8 9	mp2	$⊢ ((φ \to ((φ \to φ) \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		minimp	$⊢ ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ))))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to ((((φ \to ((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ)))) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to φ)))$
12	5 11	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 φ))$
13	6 10 12	mp2	$⊢ (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to φ$
14		minimp	$⊢ ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ))))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to φ) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \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	5 13 14	mp2	$⊢ (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to (φ \to (ψ \to χ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ))$
16		minimp-syllsimp	$⊢ ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ)) \to (φ \to (ψ \to χ))) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ))) \to ((φ \to (ψ \to χ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)))$
17	15 16	ax-mp	$⊢ (φ \to (ψ \to χ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ))$
18		minimp	$⊢ ((φ \to (ψ \to χ)) \to (((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ))) \to ((((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ))) \to ((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ)))) \to ((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ)))))) \to (((φ \to (ψ \to χ)) \to ((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ))) \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	4 17 18	mp2	$⊢ (((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$
20		minimp-syllsimp	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ))) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))$
21	19 20	ax-mp	$⊢ (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$
22		minimp	$⊢ ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))))))$
23		minimp	$⊢ (φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))$
24		minimp	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \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	23 24	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 χ))))$
26		minimp	$⊢ (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))))))) \to ((((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))) \to (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to (((((((φ \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	22 25 26	mp2	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to (((((((φ \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		minimp-syllsimp	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((φ \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		minimp-syllsimp	$⊢ (((((φ \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to (((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))) \to (((((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ)) \to ((φ \to (ψ \to χ)) \to (φ \to χ))) \to ((φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))))) \to (((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to (((((((φ \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	27 28 29	mp2	$⊢ ((φ \to ψ) \to (((((φ \to φ) \to (((φ \to φ) \to (φ \to φ)) \to (φ \to φ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))) \to (((((((φ \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	3 21 30	mp2	$⊢ (φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$

Metamath Proof Explorer

Theorem minimp-ax2c

Proof