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

Proof

Step Hyp Ref Expression
1 pm2.01d.1 
 |-  ( ph -> ( ps -> -. ps ) )
2 id 
 |-  ( -. ps -> -. ps )
3 1 2 pm2.61d1 
 |-  ( ph -> -. ps )