Theorem ancomd 454

Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)

Hypothesis

Ref	Expression
ancomd.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
ancomd	⊢ (𝜑 → (𝜒 ∧ 𝜓))

Proof of Theorem ancomd

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		ancom 453	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 210	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  simprd  488  jccil  515  2reu5  3660  relbrcnvg  5813  soxp  7634  ressuppssdif  7660  supp0cosupp0OLD  7682  imacosuppOLD  7684  relelec  8140  undifixp  8301  funsnfsupp  8658  infmo  8760  fpwwe2lem13  9868  nqpr  10240  infregelb  11432  ssfzunsnext  12774  focdmex  13532  hashf1rn  13534  hashge2el2dif  13655  ccatsymb  13751  pfxsuffeqwrdeq  13886  pfxccatin12  13940  swrdccatin12OLD  13941  swrdccat3OLD  13943  cshwidxmod  14033  cshweqdif2  14049  pfxco  14068  sinbnd  15399  cosbnd  15400  lcmfun  15851  divgcdcoprmex  15872  cncongr1  15873  vfermltlALT  16001  setsstruct2  16383  funcsetcestrclem8  17282  fullsetcestrc  17286  mat1dim0  20801  mat1dimid  20802  mat1dimscm  20803  mat1dimmul  20804  dmatmul  20825  scmatcrng  20849  1marepvsma1  20911  cramerimplem1  21011  cramerimplem2  21012  cpmatacl  21043  cpmatmcllem  21045  decpmatmul  21099  pmatcollpwscmatlem1  21116  chpmat1dlem  21162  chfacfscmul0  21185  chfacfpmmul0  21189  lpbl  22831  metustsym  22883  sincosq2sgn  24803  sincosq4sgn  24805  ercgrg  26020  subupgr  26787  nbgr2vtx1edg  26850  nbuhgr2vtx1edgb  26852  cplgr3v  26935  wlkreslemOLD  27172  pthdivtx  27233  usgr2wlkspthlem1  27261  usgr2wlkspthlem2  27262  wwlknbp  27343  clwwlkccat  27511  clwlkclwwlklem2a  27519  eleclclwwlknlem2  27600  clwwlknonwwlknonb  27649  clwlknon2num  27936  numclwlk1lem1  27937  numclwlk1lem2  27938  numclwwlk7  27963  frgrreg  27966  shorth  28868  trleile  30411  oddpwdc  31289  bnj1098  31735  bnj999  31908  bnj1118  31933  segcon2  33127  pibt2  34179  lsateln0  35616  cvrcmp2  35905  dalemswapyz  36277  lhprelat3N  36661  cdleme28b  36992  qirropth  38942  nzin  40107  sigaraf  42576  sigarmf  42577  sigaras  42578  sigarms  42579  sigariz  42586  afvelrn  42808  elfzelfzlble  42962  prproropf1olem4  43071  prprelprb  43082  fmtnoprmfac2  43132  flsqrt  43159  proththd  43182  evensumeven  43275  evengpop3  43366  evengpoap3  43367  nnsum4primeseven  43368  nnsum4primesevenALTV  43369  tgoldbach  43385  uspgrsprfo  43426  mgmhmf1o  43457  rnghmf1o  43573  c0snmgmhm  43584  lmodvsmdi  43831  ply1mulgsumlem1  43842  lindslinindsimp1  43914  lindsrng01  43925  ldepspr  43930  digexp  44070  dig1  44071  rrx2pnedifcoorneorr  44107  rrxsphere  44138  setrec1lem3  44194