Metamath Proof Explorer


Theorem pm2.18da

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

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

Proof

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