Metamath Proof Explorer

Theorem con3d

Description: A contraposition deduction. Deduction form of con3 . (Contributed by NM, 10-Jan-1993)

Ref Expression
Hypothesis con3d.1 
|- ( ph -> ( ps -> ch ) )
Assertion con3d 
|- ( ph -> ( -. ch -> -. ps ) )

Proof

Step Hyp Ref Expression
1 con3d.1 
 |-  ( ph -> ( ps -> ch ) )
2 notnotr 
 |-  ( -. -. ps -> ps )
3 2 1 syl5 
 |-  ( ph -> ( -. -. ps -> ch ) )
4 3 con1d 
 |-  ( ph -> ( -. ch -> -. ps ) )