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  3766  relbrcnvg  6125  soxp  8152  ressuppssdif  8208  relelec  8790  undifixp  8972  funsnfsupp  9429  infmo  9532  fpwwe2lem12  10679  nqpr  11051  infregelb  12249  ssfzunsnext  13605  hashf1rn  14387  hashge2el2dif  14515  pfxccatin12  14767  cshwidxmod  14837  cshweqdif2  14853  pfxco  14873  sinbnd  16212  cosbnd  16213  lcmfun  16678  divgcdcoprmex  16699  cncongr1  16700  vfermltlALT  16835  setsstruct2  17207  funcsetcestrclem8  18217  fullsetcestrc  18221  mgmhmf1o  18725  smndex1iidm  18926  cyccom  19233  rnghmf1o  20468  c0snmgmhm  20478  quscrng  21310  mat1dim0  22494  mat1dimid  22495  mat1dimscm  22496  mat1dimmul  22497  dmatmul  22518  scmatcrng  22542  1marepvsma1  22604  cramerimplem1  22704  cramerimplem2  22705  cpmatacl  22737  cpmatmcllem  22739  decpmatmul  22793  pmatcollpwscmatlem1  22810  chpmat1dlem  22856  chfacfscmul0  22879  chfacfpmmul0  22883  lpbl  24531  metustsym  24583  sincosq2sgn  26555  sincosq4sgn  26557  ercgrg  28539  subupgr  29318  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  cplgr3v  29466  pthdivtx  29761  usgr2wlkspthlem1  29789  usgr2wlkspthlem2  29790  wwlknbp  29871  clwlkclwwlklem2a  30026  eleclclwwlknlem2  30089  clwwlknonwwlknonb  30134  clwlknon2num  30396  numclwlk1lem1  30397  numclwlk1lem2  30398  numclwwlk7  30419  frgrreg  30422  shorth  31323  trleile  32945  oddpwdc  34335  bnj1098  34775  bnj999  34950  bnj1118  34976  segcon2  36086  pibt2  37399  lsateln0  38976  cvrcmp2  39265  dalemswapyz  39638  lhprelat3N  40022  cdleme28b  40353  qirropth  42895  onsucf1lem  43258  omlim2  43288  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcatrev  43337  nzin  44313  sigaraf  46808  sigarmf  46809  sigaras  46810  sigarms  46811  sigariz  46818  f1cof1b  47026  afvelrn  47117  elfzelfzlble  47270  prproropf1olem4  47430  prprelprb  47441  fmtnoprmfac2  47491  flsqrt  47517  proththd  47538  evensumeven  47631  evengpop3  47722  evengpoap3  47723  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  tgoldbach  47741  uhgrimisgrgric  47836  lmodvsmdi  48223  ply1mulgsumlem1  48231  lindslinindsimp1  48302  lindsrng01  48313  ldepspr  48318  digexp  48456  dig1  48457  rrx2pnedifcoorneorr  48566  rrxsphere  48597  setrec1lem3  48919