Metamath Proof Explorer


Theorem pm2.01d

Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993) (Proof shortened by Wolf Lammen, 5-Mar-2013)

Ref Expression
Hypothesis pm2.01d.1 φ ψ ¬ ψ
Assertion pm2.01d φ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm2.01d.1 φ ψ ¬ ψ
2 id ¬ ψ ¬ ψ
3 1 2 pm2.61d1 φ ¬ ψ