Metamath Proof Explorer

Theorem con1d

Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992)

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

Proof

Step Hyp Ref Expression
1 con1d.1 
 |-  ( ph -> ( -. ps -> ch ) )
2 notnot 
 |-  ( ch -> -. -. ch )
3 1 2 syl6 
 |-  ( ph -> ( -. ps -> -. -. ch ) )
4 3 con4d 
 |-  ( ph -> ( -. ch -> ps ) )