adh-minimp-jarr-ax2c-lem3

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

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

Proof

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

Metamath Proof Explorer

Theorem adh-minimp-jarr-ax2c-lem3

Proof