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  1743  sbnOLD  2083  ax13fromc9  2206  mo2icl  3143  sbcrext  3274  uzwo  10922  uzwoOLD  10923  hmeofval  19336  alexsubALTlem4  19627  nb3graprlem2  23365  cvnbtwn  25695  otsndisj  30136  frgrancvvdeqlem1  30628  frgrancvvdeqlemA  30635  frgrancvvdeqlemC  30637  frgrawopreglem4  30645  2spotdisj  30659  snnen2o  30743  ssnn0fi  30751  not12an2impnot1  31286
  Copyright terms: Public domain W3C validator