Theorem ancomd 462

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simprd  496  jccil  527  2reu5  3706  relbrcnvg  6064  soxp  8076  ressuppssdif  8132  relelec  8688  undifixp  8879  funsnfsupp  9302  infmo  9407  fpwwe2lem12  10563  nqpr  10935  infregelb  12138  ssfzunsnext  13521  hashf1rn  14312  hashge2el2dif  14440  pfxccatin12  14693  cshwidxmod  14763  cshweqdif2  14779  pfxco  14798  sinbnd  16145  cosbnd  16146  lcmfun  16612  divgcdcoprmex  16633  cncongr1  16634  vfermltlALT  16771  setsstruct2  17142  funcsetcestrclem8  18126  fullsetcestrc  18130  chnccat  18590  mgmhmf1o  18666  smndex1iidm  18867  cyccom  19176  rnghmf1o  20430  c0snmgmhm  20440  quscrng  21283  mat1dim0  22463  mat1dimid  22464  mat1dimscm  22465  mat1dimmul  22466  dmatmul  22487  scmatcrng  22511  1marepvsma1  22573  cramerimplem1  22673  cramerimplem2  22674  cpmatacl  22706  cpmatmcllem  22708  decpmatmul  22762  pmatcollpwscmatlem1  22779  chpmat1dlem  22825  chfacfscmul0  22848  chfacfpmmul0  22852  lpbl  24493  metustsym  24545  sincosq2sgn  26488  sincosq4sgn  26490  ercgrg  28610  subupgr  29381  nbgr2vtx1edg  29444  nbuhgr2vtx1edgb  29446  cplgr3v  29529  pthdivtx  29820  usgr2wlkspthlem1  29850  usgr2wlkspthlem2  29851  wwlknbp  29935  clwlkclwwlklem2a  30093  eleclclwwlknlem2  30156  clwwlknonwwlknonb  30201  clwlknon2num  30463  numclwlk1lem1  30464  numclwlk1lem2  30465  numclwwlk7  30486  frgrreg  30489  shorth  31391  trleile  33057  oddpwdc  34545  bnj1098  34973  bnj999  35147  bnj1118  35173  segcon2  36334  pibt2  37780  lsateln0  39488  cvrcmp2  39777  dalemswapyz  40149  lhprelat3N  40533  cdleme28b  40864  qirropth  43354  onsucf1lem  43715  omlim2  43745  tfsconcatlem  43782  tfsconcatrn  43788  tfsconcatrev  43794  nzin  44763  sigaraf  47297  sigarmf  47298  sigaras  47299  sigarms  47300  sigariz  47307  f1cof1b  47541  afvelrn  47632  elfzelfzlble  47785  prproropf1olem4  47982  prprelprb  47993  fmtnoprmfac2  48046  flsqrt  48072  proththd  48093  evensumeven  48199  evengpop3  48290  evengpoap3  48291  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  tgoldbach  48309  uhgrimisgrgric  48423  gpgedg2ov  48558  gpgedg2iv  48559  lmodvsmdi  48871  ply1mulgsumlem1  48878  lindslinindsimp1  48949  lindsrng01  48960  ldepspr  48965  digexp  49099  dig1  49100  rrx2pnedifcoorneorr  49209  rrxsphere  49240  setrec1lem3  50180