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  2973  elres  4990  relbrcnvg  5052  soxp  6228  relelec  6700  undifixp  6852  fpwwe2lem13  8264  nqpr  8638  sinbnd  12460  cosbnd  12461  lpbl  18049  sincosq2sgn  19867  sincosq4sgn  19869  shorth  21874  segcon2  24728  invaddvec  25467  dualded  25783  homib  25796  qirropth  26993  cnfex  27699  sigaraf  27843  sigarmf  27844  sigaras  27845  sigarms  27846  sigariz  27853  afvelrn  28030  1to3vfriswmgra  28185  bnj1098  28815  bnj999  28989  bnj1118  29014  lsateln0  29185  cvrcmp2  29474  dalemswapyz  29845  lhprelat3N  30229  cdleme28b  30560
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