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  3764  relbrcnvg  6123  soxp  8154  ressuppssdif  8210  relelec  8792  undifixp  8974  funsnfsupp  9432  infmo  9535  fpwwe2lem12  10682  nqpr  11054  infregelb  12252  ssfzunsnext  13609  hashf1rn  14391  hashge2el2dif  14519  pfxccatin12  14771  cshwidxmod  14841  cshweqdif2  14857  pfxco  14877  sinbnd  16216  cosbnd  16217  lcmfun  16682  divgcdcoprmex  16703  cncongr1  16704  vfermltlALT  16840  setsstruct2  17211  funcsetcestrclem8  18207  fullsetcestrc  18211  mgmhmf1o  18713  smndex1iidm  18914  cyccom  19221  rnghmf1o  20452  c0snmgmhm  20462  quscrng  21293  mat1dim0  22479  mat1dimid  22480  mat1dimscm  22481  mat1dimmul  22482  dmatmul  22503  scmatcrng  22527  1marepvsma1  22589  cramerimplem1  22689  cramerimplem2  22690  cpmatacl  22722  cpmatmcllem  22724  decpmatmul  22778  pmatcollpwscmatlem1  22795  chpmat1dlem  22841  chfacfscmul0  22864  chfacfpmmul0  22868  lpbl  24516  metustsym  24568  sincosq2sgn  26541  sincosq4sgn  26543  ercgrg  28525  subupgr  29304  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  cplgr3v  29452  pthdivtx  29747  usgr2wlkspthlem1  29777  usgr2wlkspthlem2  29778  wwlknbp  29862  clwlkclwwlklem2a  30017  eleclclwwlknlem2  30080  clwwlknonwwlknonb  30125  clwlknon2num  30387  numclwlk1lem1  30388  numclwlk1lem2  30389  numclwwlk7  30410  frgrreg  30413  shorth  31314  trleile  32961  oddpwdc  34356  bnj1098  34797  bnj999  34972  bnj1118  34998  segcon2  36106  pibt2  37418  lsateln0  38996  cvrcmp2  39285  dalemswapyz  39658  lhprelat3N  40042  cdleme28b  40373  qirropth  42919  onsucf1lem  43282  omlim2  43312  tfsconcatlem  43349  tfsconcatrn  43355  tfsconcatrev  43361  nzin  44337  sigaraf  46868  sigarmf  46869  sigaras  46870  sigarms  46871  sigariz  46878  f1cof1b  47089  afvelrn  47180  elfzelfzlble  47333  prproropf1olem4  47493  prprelprb  47504  fmtnoprmfac2  47554  flsqrt  47580  proththd  47601  evensumeven  47694  evengpop3  47785  evengpoap3  47786  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  tgoldbach  47804  uhgrimisgrgric  47899  lmodvsmdi  48295  ply1mulgsumlem1  48303  lindslinindsimp1  48374  lindsrng01  48385  ldepspr  48390  digexp  48528  dig1  48529  rrx2pnedifcoorneorr  48638  rrxsphere  48669  setrec1lem3  49208