Metamath Proof Explorer

Theorem adh-minim-ax2c

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

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

Proof

Step	Hyp	Ref	Expression
1		adh-minim-ax2-lem5	$⊢ (φ \to ψ) \to ((((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ) \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ)))$
2		adh-minim-ax2-lem6	$⊢ ((((σ \to ρ) \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		adh-minim-ax2-lem6	$⊢ (((((σ \to ρ) \to μ) \to ((ρ \to (μ \to λ)) \to (ρ \to λ))) \to ((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ)) \to ((((σ \to ρ) \to μ) \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	2 3	ax-mp	$⊢ ((((σ \to ρ) \to μ) \to ((ρ \to (μ \to λ)) \to (ρ \to λ))) \to ((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ)) \to φ$
5		adh-minim-ax1-ax2-lem4	$⊢ (((((σ \to ρ) \to μ) \to ((ρ \to (μ \to λ)) \to (ρ \to λ))) \to ((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \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	4 5	ax-mp	$⊢ (((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ) \to (φ \to ψ)) \to (((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ) \to ψ)$
7		adh-minim-ax1-ax2-lem4	$⊢ ((((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ) \to (φ \to ψ)) \to (((((θ \to τ) \to η) \to ((τ \to (η \to ζ)) \to (τ \to ζ))) \to φ) \to ψ)) \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	6 7	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 χ)))$
9	1 8	ax-mp	$⊢ (φ \to ψ) \to ((φ \to (ψ \to χ)) \to (φ \to χ))$