Metamath Proof Explorer

Theorem con3rr3

Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 con3rr3.1 
 |-  ( ph -> ( ps -> ch ) )
2 1 con3d 
 |-  ( ph -> ( -. ch -> -. ps ) )
3 2 com12 
 |-  ( -. ch -> ( ph -> -. ps ) )