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

Theorem ancomd 439
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
Hypothesis
Ref Expression
ancomd.1  |-  ( ph  ->  ( ps  /\  ch ) )
Assertion
Ref Expression
ancomd  |-  ( ph  ->  ( ch  /\  ps ) )

Proof of Theorem ancomd
StepHypRef Expression
1 ancomd.1 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
2 ancom 438 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 189 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simprd  450  2reu5  3085  elres  5121  relbrcnvg  5183  soxp  6395  relelec  6881  undifixp  7034  fpwwe2lem13  8450  nqpr  8824  sinbnd  12708  cosbnd  12709  lpbl  18423  metustsym  18475  sincosq2sgn  20274  sincosq4sgn  20276  shorth  22645  segcon2  25753  qirropth  26662  sigaraf  27511  sigarmf  27512  sigaras  27513  sigarms  27514  sigariz  27521  afvelrn  27701  1to3vfriswmgra  27760  frgranbnb  27773  frgrawopreglem5  27800  frgrawopreg  27801  bnj1098  28492  bnj999  28666  bnj1118  28691  lsateln0  29110  cvrcmp2  29399  dalemswapyz  29770  lhprelat3N  30154  cdleme28b  30485
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator