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

Theorem con3rr3 128
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 125 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32com12 27 1  |-  ( -. 
ch  ->  ( ph  ->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  impi  140  ax12b  1674  equs5e  1841  ax12  1888  ax10lem2  1890  sbn  2015  ax12from12o  2108  mo2icl  2957  uzwo  10297  uzwoOLD  10298  hmeofval  17465  alexsubALTlem4  17760  cvnbtwn  22882  efilcp  25655  nb3graprlem2  28288  sbnNEW7  29537  ax9lem15  29776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator