Metamath Proof Explorer

Theorem adh-minimp-jarr-imim1-ax2c-lem1

Description: First lemma for the derivation of jarr , imim1 , and a commuted form of ax-2 , and indirectly ax-1 and ax-2 , from adh-minimp and ax-mp . Polish prefix notation: CCpqCCCrpCqsCps . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		adh-minimp	$⊢ η \to ((ζ \to σ) \to (((ρ \to ζ) \to (σ \to μ)) \to (ζ \to μ)))$
2		adh-minimp	$⊢ (η \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 θ))$