Metamath Proof Explorer


Theorem pm2.01da

Description: Deduction based on reductio ad absurdum. See pm2.01 . (Contributed by Mario Carneiro, 9-Feb-2017)

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

Proof

Step Hyp Ref Expression
1 pm2.01da.1 φ ψ ¬ ψ
2 1 ex φ ψ ¬ ψ
3 2 pm2.01d φ ¬ ψ