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

Theorem ancomd 438
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 437 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 188 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simprd  449  2reu5  2986  elres  5006  relbrcnvg  5068  soxp  6244  relelec  6716  undifixp  6868  fpwwe2lem13  8280  nqpr  8654  sinbnd  12476  cosbnd  12477  lpbl  18065  sincosq2sgn  19883  sincosq4sgn  19885  shorth  21890  segcon2  24800  invaddvec  25570  dualded  25886  homib  25899  qirropth  27096  cnfex  27802  sigaraf  27946  sigarmf  27947  sigaras  27948  sigarms  27949  sigariz  27956  afvelrn  28136  1to3vfriswmgra  28431  bnj1098  29131  bnj999  29305  bnj1118  29330  lsateln0  29807  cvrcmp2  30096  dalemswapyz  30467  lhprelat3N  30851  cdleme28b  31182
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 177  df-an 360
  Copyright terms: Public domain W3C validator