MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancomd Structured version   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  3134  elres  5173  relbrcnvg  5235  soxp  6451  relelec  6937  undifixp  7090  fpwwe2lem13  8509  nqpr  8883  sinbnd  12773  cosbnd  12774  lpbl  18525  metustsymOLD  18583  metustsym  18584  sincosq2sgn  20399  sincosq4sgn  20401  shorth  22789  segcon2  26031  qirropth  26962  sigaraf  27810  sigarmf  27811  sigaras  27812  sigarms  27813  sigariz  27820  afvelrn  27999  swrdccatin12  28180  swrdccat3  28181  usgra2adedgwlk  28269  usgra2adedgwlkon  28270  1to3vfriswmgra  28334  frgranbnb  28347  frgrawopreglem5  28374  frgrawopreg  28375  bnj1098  29091  bnj999  29265  bnj1118  29290  lsateln0  29730  cvrcmp2  30019  dalemswapyz  30390  lhprelat3N  30774  cdleme28b  31105
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