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 ⊢ φ → ψ → χ → ψ → θ → φ → χ