Theorem ancomd 467

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

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		ancom 466	. 2 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
3	1, 2	sylib 208	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  simprd  479  jccil  563  2reu5  3416  elpwdifsn  4319  elres  5435  relbrcnvg  5504  frnssb  6391  soxp  7290  ressuppssdif  7316  supp0cosupp0  7334  imacosupp  7335  relelec  7787  undifixp  7944  funsnfsupp  8299  infmo  8401  fpwwe2lem13  9464  nqpr  9836  infregelb  11007  ssfzunsnext  12386  focdmex  13139  hashf1rn  13142  hashge2el2dif  13262  ccatval3  13363  ccatsymb  13366  ccatalpha  13375  swrdccatin12  13491  swrdccat3  13492  cshwidxmod  13549  cshweqdif2  13565  sinbnd  14910  cosbnd  14911  dvdsdivcl  15038  nn0ehalf  15095  nn0oddm1d2  15101  nnoddm1d2  15102  sumeven  15110  lcmfun  15358  coprmgcdb  15362  ncoprmgcdne1b  15363  divgcdcoprm0  15379  divgcdcoprmex  15380  cncongr1  15381  ncoprmlnprm  15436  vfermltl  15506  vfermltlALT  15507  modprmn0modprm0  15512  dvdsprmpweqle  15590  prmgaplem4  15758  prmgaplem7  15761  setsstruct2  15896  funcsetcestrclem8  16802  fullsetcestrc  16806  ixpsnbasval  19209  mat1dim0  20279  mat1dimid  20280  mat1dimscm  20281  mat1dimmul  20282  dmatmul  20303  scmatmats  20317  scmatscm  20319  scmatmulcl  20324  scmatcrng  20327  1marepvsma1  20389  mdet1  20407  mdet0  20412  cramerimplem1  20489  cramerimplem2  20490  cramer  20497  cpmatacl  20521  cpmatmcllem  20523  decpmatmul  20577  pmatcollpwscmatlem1  20594  pmatcollpwscmat  20596  chpmat1dlem  20640  chfacfisf  20659  chfacfscmul0  20663  chfacfpmmul0  20667  lpbl  22308  metustsym  22360  sincosq2sgn  24251  sincosq4sgn  24253  lgsqrmodndvds  25078  ercgrg  25412  subupgr  26179  usgrfilem  26219  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  cplgr3v  26331  wlkreslem  26566  pthdivtx  26625  usgr2wlkspthlem1  26653  usgr2wlkspthlem2  26654  wwlknbp  26733  clwwlknbp0  26884  clwlkclwwlklem2a  26899  clwwlksnfi  26913  eleclclwwlksnlem2  26939  uhgr3cyclex  27042  eucrctshift  27103  1to3vfriswmgr  27144  frgrnbnb  27157  fusgreghash2wspv  27199  numclwwlk4  27244  numclwwlk6  27248  numclwwlk7  27249  frgrreggt1  27251  frgrreg  27252  shorth  28154  trleile  29666  oddpwdc  30416  bnj1098  30854  bnj999  31027  bnj1118  31052  segcon2  32212  lsateln0  34282  cvrcmp2  34571  dalemswapyz  34942  lhprelat3N  35326  cdleme28b  35659  qirropth  37473  nzin  38517  sigaraf  41042  sigarmf  41043  sigaras  41044  sigarms  41045  sigariz  41052  afvelrn  41248  elfzelfzlble  41331  pfxsuffeqwrdeq  41406  ccatpfx  41409  pfxccatin12  41425  pfxccat3  41426  pfxccat3a  41429  pfxco  41438  fmtnoprmfac2  41479  flsqrt  41508  proththd  41531  evensumeven  41616  evengpop3  41686  evengpoap3  41687  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  tgoldbach  41705  tgoldbachOLD  41712  uspgrsprfo  41756  mgmhmf1o  41787  rnghmf1o  41903  c0snmgmhm  41914  lmodvsmdi  42163  ply1mulgsumlem1  42174  lindslinindsimp1  42246  lindsrng01  42257  ldepspr  42262  elbigolo1  42351  digexp  42401  dig1  42402  setrec1lem3  42436