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

Theorem con3rr3 141
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 138 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32com12 32 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  151  ax13b  1859  mo2icl  3192  sbcrext  3316  otsndisj  4668  snnen2o  7714  uzwo  11173  ssnn0fi  12147  hmeofval  20715  alexsubALTlem4  21007  nb3graprlem2  25122  frgrancvvdeqlem1  25700  frgrancvvdeqlemA  25707  frgrancvvdeqlemC  25709  frgrawopreglem4  25717  2spotdisj  25731  cvnbtwn  27881  ax13fromc9  32388  not12an2impnot1  36852  nbuhgr  39157  nbgrnself2  39177  nb3grprlem2  39196
  Copyright terms: Public domain W3C validator