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  1810  ax13fromc9  2237  mo2icl  3275  sbcrext  3398  otsndisj  4741  snnen2o  7699  uzwo  11145  uzwoOLD  11146  ssnn0fi  12079  hmeofval  20428  alexsubALTlem4  20719  nb3graprlem2  24657  frgrancvvdeqlem1  25235  frgrancvvdeqlemA  25242  frgrancvvdeqlemC  25244  frgrawopreglem4  25252  2spotdisj  25266  cvnbtwn  27406  not12an2impnot1  33758
  Copyright terms: Public domain W3C validator