Metamath Proof Explorer


Theorem adh-minim-ax2-lem5

Description: Fifth lemma for the derivation of ax-2 from adh-minim and ax-mp . Polish prefix notation: CpCCCqrsCCrCstCrt . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minim-ax2-lem5 φ ψ χ θ χ θ τ χ τ

Proof

Step Hyp Ref Expression
1 adh-minim-ax1-ax2-lem4 ψ χ θ χ θ τ χ τ
2 adh-minim-ax1 ψ χ θ χ θ τ χ τ φ ψ χ θ χ θ τ χ τ
3 1 2 ax-mp φ ψ χ θ χ θ τ χ τ