Theorem ancomd 465

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  simprd  499  jccil  530  2reu5  3720  relbrcnvg  6091  soxp  8104  ressuppssdif  8160  relelec  8721  undifixp  8912  funsnfsupp  9335  infmo  9440  fpwwe2lem12  10597  nqpr  10969  infregelb  12173  ssfzunsnext  13571  hashf1rn  14362  hashge2el2dif  14490  pfxccatin12  14743  cshwidxmod  14813  cshweqdif2  14829  pfxco  14848  sinbnd  16195  cosbnd  16196  lcmfun  16662  divgcdcoprmex  16683  cncongr1  16684  vfermltlALT  16821  setsstruct2  17193  funcsetcestrclem8  18177  fullsetcestrc  18181  chnccat  18641  mgmhmf1o  18717  smndex1iidm  18918  cyccom  19227  rnghmf1o  20480  c0snmgmhm  20490  quscrng  21333  mat1dim0  22513  mat1dimid  22514  mat1dimscm  22515  mat1dimmul  22516  dmatmul  22537  scmatcrng  22561  1marepvsma1  22623  cramerimplem1  22723  cramerimplem2  22724  cpmatacl  22756  cpmatmcllem  22758  decpmatmul  22812  pmatcollpwscmatlem1  22829  chpmat1dlem  22875  chfacfscmul0  22898  chfacfpmmul0  22902  lpbl  24543  metustsym  24595  sincosq2sgn  26541  sincosq4sgn  26543  ercgrg  28663  subupgr  29434  nbgr2vtx1edg  29497  nbuhgr2vtx1edgb  29499  cplgr3v  29582  pthdivtx  29873  usgr2wlkspthlem1  29903  usgr2wlkspthlem2  29904  wwlknbp  29988  clwlkclwwlklem2a  30146  eleclclwwlknlem2  30209  clwwlknonwwlknonb  30254  clwlknon2num  30516  numclwlk1lem1  30517  numclwlk1lem2  30518  numclwwlk7  30539  frgrreg  30542  shorth  31444  trleile  33110  oddpwdc  34612  bnj1098  35043  bnj999  35217  bnj1118  35243  segcon2  36419  pibt2  37875  lsateln0  39583  cvrcmp2  39872  dalemswapyz  40244  lhprelat3N  40628  cdleme28b  40959  qirropth  43449  onsucf1lem  43810  omlim2  43840  tfsconcatlem  43877  tfsconcatrn  43883  tfsconcatrev  43889  nzin  44858  sigaraf  47391  sigarmf  47392  sigaras  47393  sigarms  47394  sigariz  47401  f1cof1b  47635  afvelrn  47726  elfzelfzlble  47879  prproropf1olem4  48076  prprelprb  48087  fmtnoprmfac2  48140  flsqrt  48166  proththd  48187  evensumeven  48293  evengpop3  48384  evengpoap3  48385  nnsum4primeseven  48386  nnsum4primesevenALTV  48387  tgoldbach  48403  uhgrimisgrgric  48517  gpgedg2ov  48652  gpgedg2iv  48653  lmodvsmdi  48965  ply1mulgsumlem1  48972  lindslinindsimp1  49043  lindsrng01  49054  ldepspr  49059  digexp  49193  dig1  49194  rrx2pnedifcoorneorr  49303  rrxsphere  49334  setrec1lem3  50274