Theorem ancomd 461

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 460	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 218	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprd  495  jccil  522  2reu5  3780  relbrcnvg  6135  soxp  8170  ressuppssdif  8226  relelec  8810  undifixp  8992  funsnfsupp  9461  infmo  9564  fpwwe2lem12  10711  nqpr  11083  infregelb  12279  ssfzunsnext  13629  hashf1rn  14401  hashge2el2dif  14529  pfxccatin12  14781  cshwidxmod  14851  cshweqdif2  14867  pfxco  14887  sinbnd  16228  cosbnd  16229  lcmfun  16692  divgcdcoprmex  16713  cncongr1  16714  vfermltlALT  16849  setsstruct2  17221  funcsetcestrclem8  18231  fullsetcestrc  18235  mgmhmf1o  18738  smndex1iidm  18936  cyccom  19243  rnghmf1o  20478  c0snmgmhm  20488  quscrng  21316  mat1dim0  22500  mat1dimid  22501  mat1dimscm  22502  mat1dimmul  22503  dmatmul  22524  scmatcrng  22548  1marepvsma1  22610  cramerimplem1  22710  cramerimplem2  22711  cpmatacl  22743  cpmatmcllem  22745  decpmatmul  22799  pmatcollpwscmatlem1  22816  chpmat1dlem  22862  chfacfscmul0  22885  chfacfpmmul0  22889  lpbl  24537  metustsym  24589  sincosq2sgn  26559  sincosq4sgn  26561  ercgrg  28543  subupgr  29322  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  cplgr3v  29470  pthdivtx  29765  usgr2wlkspthlem1  29793  usgr2wlkspthlem2  29794  wwlknbp  29875  clwlkclwwlklem2a  30030  eleclclwwlknlem2  30093  clwwlknonwwlknonb  30138  clwlknon2num  30400  numclwlk1lem1  30401  numclwlk1lem2  30402  numclwwlk7  30423  frgrreg  30426  shorth  31327  trleile  32944  oddpwdc  34319  bnj1098  34759  bnj999  34934  bnj1118  34960  segcon2  36069  pibt2  37383  lsateln0  38951  cvrcmp2  39240  dalemswapyz  39613  lhprelat3N  39997  cdleme28b  40328  qirropth  42864  onsucf1lem  43231  omlim2  43261  tfsconcatlem  43298  tfsconcatrn  43304  tfsconcatrev  43310  nzin  44287  sigaraf  46774  sigarmf  46775  sigaras  46776  sigarms  46777  sigariz  46784  f1cof1b  46992  afvelrn  47083  elfzelfzlble  47236  prproropf1olem4  47380  prprelprb  47391  fmtnoprmfac2  47441  flsqrt  47467  proththd  47488  evensumeven  47581  evengpop3  47672  evengpoap3  47673  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  tgoldbach  47691  uhgrimisgrgric  47783  lmodvsmdi  48107  ply1mulgsumlem1  48115  lindslinindsimp1  48186  lindsrng01  48197  ldepspr  48202  digexp  48341  dig1  48342  rrx2pnedifcoorneorr  48451  rrxsphere  48482  setrec1lem3  48781