MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3rr3 Structured version   Unicode version

Theorem con3rr3 136
Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
Hypothesis
Ref Expression
con3rr3.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
con3rr3  |-  ( -. 
ch  ->  ( ph  ->  -. 
ps ) )

Proof of Theorem con3rr3
StepHypRef Expression
1 con3rr3.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21con3d 133 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32com12 31 1  |-  ( -. 
ch  ->  ( ph  ->  -. 
ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  impi  148  ax13b  1791  ax13fromc9  2221  mo2icl  3264  sbcrext  3396  otsndisj  4742  snnen2o  7708  uzwo  11155  uzwoOLD  11156  ssnn0fi  12076  hmeofval  20237  alexsubALTlem4  20528  nb3graprlem2  24430  frgrancvvdeqlem1  25008  frgrancvvdeqlemA  25015  frgrancvvdeqlemC  25017  frgrawopreglem4  25025  2spotdisj  25039  cvnbtwn  27183  not12an2impnot1  33213
  Copyright terms: Public domain W3C validator