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

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

Proof of Theorem con3rr3
StepHypRef Expression
1 con3rr3.1 . . 3
21con3d 133 . 2
32com12 31 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  impi  148  ax13b  1805  ax13fromc9  2235  mo2icl  3278  sbcrext  3410  otsndisj  4757  snnen2o  7726  uzwo  11173  uzwoOLD  11174  ssnn0fi  12094  hmeofval  20259  alexsubALTlem4  20550  nb3graprlem2  24452  frgrancvvdeqlem1  25030  frgrancvvdeqlemA  25037  frgrancvvdeqlemC  25039  frgrawopreglem4  25047  2spotdisj  25061  cvnbtwn  27205  not12an2impnot1  33345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator