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  1655  equs5e  1829  ax10lem2  1877  sbn  2002  ax12  2095  mo2icl  2944  uzwo  10281  uzwoOLD  10282  hmeofval  17449  alexsubALTlem4  17744  cvnbtwn  22866  efilcp  25552  ax9lem15  29154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator