Metamath Proof Explorer

Theorem adh-minimp-ax2

Description: Derivation of ax-2 from adh-minimp and ax-mp . Polish prefix notation: CCpCqrCCpqCpr . (Contributed by BJ, 4-Apr-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minimp-ax2 ⊢ φ → ψ → χ → φ → ψ → φ → χ

Proof

Step Hyp Ref Expression
1 adh-minimp-ax2-lem4 ⊢ φ → ψ → χ → φ → ψ → φ → ψ → χ → φ → χ → φ → ψ → φ → χ
2 adh-minimp-ax2c ⊢ φ → ψ → φ → ψ → χ → φ → χ
3 adh-minimp-ax2-lem4 ⊢ φ → ψ → φ → ψ → χ → φ → χ → φ → ψ → χ → φ → ψ → φ → ψ → χ → φ → χ → φ → ψ → φ → χ → φ → ψ → χ → φ → ψ → φ → χ
4 2 3 ax-mp ⊢ φ → ψ → χ → φ → ψ → φ → ψ → χ → φ → χ → φ → ψ → φ → χ → φ → ψ → χ → φ → ψ → φ → χ
5 1 4 ax-mp ⊢ φ → ψ → χ → φ → ψ → φ → χ