Metamath Proof Explorer


Theorem pm2.24d

Description: Deduction form of pm2.24 . (Contributed by NM, 30-Jan-2006)

Ref Expression
Hypothesis pm2.24d.1 ⊢ φ → ψ
Assertion pm2.24d ⊢ φ → ¬ ψ → χ

Proof

Step Hyp Ref Expression
1 pm2.24d.1 ⊢ φ → ψ
2 1 a1d ⊢ φ → ¬ χ → ψ
3 2 con1d ⊢ φ → ¬ ψ → χ