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

Theorem ancomd 451
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 450 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 196 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  simprd  463  jccil  540  2reu5  3275  elres  5256  relbrcnvg  5318  soxp  6798  ressuppssdif  6823  supp0cosupp0  6841  imacosupp  6842  relelec  7254  undifixp  7412  funsnfsupp  7758  fpwwe2lem13  8923  nqpr  9297  hashge2el2dif  12305  ccatsymb  12402  swrdccatin12  12503  swrdccat3  12504  cshwidxmod  12561  cshweqdif2  12574  sinbnd  13585  cosbnd  13586  modprmn0modprm0  13996  ixpsnbasval  17416  1marepvsma1  18524  mdet1  18542  mdet0  18547  cramerimplem1  18624  cramerimplem2  18625  cramer  18632  lpbl  20213  metustsymOLD  20271  metustsym  20272  sincosq2sgn  22097  sincosq4sgn  22099  shorth  24870  trleile  26292  oddpwdc  26901  segcon2  28300  qirropth  29417  sigaraf  30057  sigarmf  30058  sigaras  30059  sigarms  30060  sigariz  30067  afvelrn  30242  elfzelfzlble  30377  usgra2adedgwlk  30474  usgra2adedgwlkon  30475  clwlkisclwwlklem2a  30615  eleclclwwlknlem2  30659  1to3vfriswmgra  30767  frgranbnb  30780  frgrawopreglem5  30809  frgrawopreg  30810  numclwlk1lem2fv  30854  numclwlk2lem2fv  30865  numclwwlk4  30871  numclwwlk5  30873  numclwwlk6  30874  numclwwlk7  30875  lmodvsmdi  30987  ply1mulgsumlem1  31018  mat1dim0  31055  mat1dimid  31056  mat1dimscm  31057  mat1dimmul  31058  dmatmul  31075  scmatcrng  31087  lindslinindsimp1  31143  lindsrng01  31154  ldepspr  31159  cpmatacl  31225  cpmatmcllem  31227  decpmatmul  31279  pmatcollpwscmatlem1  31296  pmatcollpwscmat  31298  cpmat1dlem  31341  chfacfisf  31360  chfacfscmul0  31364  chfacfpmmul0  31368  bnj1098  32129  bnj999  32302  bnj1118  32327  lsateln0  32998  cvrcmp2  33287  dalemswapyz  33658  lhprelat3N  34042  cdleme28b  34373
  Copyright terms: Public domain W3C validator