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

Theorem con3rr3 131
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 128 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32com12 30 1  |-  ( -. 
ch  ->  ( ph  ->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  impi  143  ax12b  1702  equs5eOLD  1912  ax12OLD  2021  ax10lem2OLD  2027  sbnOLD  2133  ax12from12o  2235  mo2icl  3115  uzwo  10541  uzwoOLD  10542  hmeofval  17792  alexsubALTlem4  18083  nb3graprlem2  21463  cvnbtwn  23791  otsndisj  28068  frgrancvvdeqlem1  28481  frgrancvvdeqlemA  28488  frgrancvvdeqlemC  28490  frgrawopreglem4  28498  2spotdisj  28512  not12an2impnot1  28721  sbnNEW7  29624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator