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