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  1754  sbnOLD  2106  ax13fromc9  2228  mo2icl  3282  sbcrext  3414  otsndisj  4752  snnen2o  7706  uzwo  11144  uzwoOLD  11145  ssnn0fi  12062  hmeofval  20022  alexsubALTlem4  20313  nb3graprlem2  24156  frgrancvvdeqlem1  24735  frgrancvvdeqlemA  24742  frgrancvvdeqlemC  24744  frgrawopreglem4  24752  2spotdisj  24766  cvnbtwn  26909  not12an2impnot1  32443
  Copyright terms: Public domain W3C validator