Metamath Proof Explorer


Theorem adh-minim-ax1-ax2-lem3

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

Ref Expression
Assertion adh-minim-ax1-ax2-lem3 φ ψ χ ψ θ φ χ

Proof

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