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
|- ( ( ph /\ ps ) -> -. ps )
Assertion pm2.01da
|- ( ph -> -. ps )

Proof

Step Hyp Ref Expression
1 pm2.01da.1
 |-  ( ( ph /\ ps ) -> -. ps )
2 1 ex
 |-  ( ph -> ( ps -> -. ps ) )
3 2 pm2.01d
 |-  ( ph -> -. ps )