This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.65d

Description: Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994) (Proof shortened by Wolf Lammen, 26-May-2013)

Ref Expression
Hypotheses pm2.65d.1 
|- ( ph -> ( ps -> ch ) )
pm2.65d.2 
|- ( ph -> ( ps -> -. ch ) )
Assertion pm2.65d 
|- ( ph -> -. ps )

Proof

Step Hyp Ref Expression
1 pm2.65d.1 
 |-  ( ph -> ( ps -> ch ) )
2 pm2.65d.2 
 |-  ( ph -> ( ps -> -. ch ) )
3 2 1 nsyld 
 |-  ( ph -> ( ps -> -. ps ) )
4 3 pm2.01d 
 |-  ( ph -> -. ps )