Metamath Proof Explorer

Theorem adh-minimp-ax2c

Description: Derivation of a commuted form of ax-2 from adh-minimp and ax-mp . Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		adh-minimp-jarr-ax2c-lem3	$⊢ (((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to φ$
2		adh-minimp-jarr-imim1-ax2c-lem1	$⊢ ((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to φ) \to ((((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \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 χ))) \to ((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to (ψ \to χ))$
4		adh-minimp-sylsimp	$⊢ ((((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to (((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ)) \to (φ \to (ψ \to χ))) \to ((((θ \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 χ))$
6		adh-minimp-jarr-imim1-ax2c-lem1	$⊢ ((φ \to (ψ \to χ)) \to ((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to (ψ \to χ))) \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	5 6	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 χ))$
8		adh-minimp-sylsimp	$⊢ ((((φ \to (ψ \to χ)) \to (φ \to (ψ \to χ))) \to (((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to (ψ \to χ)) \to (φ \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 χ))$
10		adh-minimp-jarr-imim1-ax2c-lem1	$⊢ (φ \to ψ) \to (((((θ \to τ) \to (((η \to θ) \to (τ \to ζ)) \to (θ \to ζ))) \to φ) \to (ψ \to χ)) \to (φ \to χ))$
11		adh-minimp-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 χ))))$
12	10 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 χ)))$
13	9 12	ax-mp	$⊢ (φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$