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 φ ¬ ψ χ