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  3718  relbrcnvg  6072  soxp  8081  ressuppssdif  8137  relelec  8693  undifixp  8884  funsnfsupp  9307  infmo  9412  fpwwe2lem12  10565  nqpr  10937  infregelb  12138  ssfzunsnext  13497  hashf1rn  14287  hashge2el2dif  14415  pfxccatin12  14668  cshwidxmod  14738  cshweqdif2  14754  pfxco  14773  sinbnd  16117  cosbnd  16118  lcmfun  16584  divgcdcoprmex  16605  cncongr1  16606  vfermltlALT  16742  setsstruct2  17113  funcsetcestrclem8  18097  fullsetcestrc  18101  chnccat  18561  mgmhmf1o  18637  smndex1iidm  18838  cyccom  19144  rnghmf1o  20400  c0snmgmhm  20410  quscrng  21250  mat1dim0  22429  mat1dimid  22430  mat1dimscm  22431  mat1dimmul  22432  dmatmul  22453  scmatcrng  22477  1marepvsma1  22539  cramerimplem1  22639  cramerimplem2  22640  cpmatacl  22672  cpmatmcllem  22674  decpmatmul  22728  pmatcollpwscmatlem1  22745  chpmat1dlem  22791  chfacfscmul0  22814  chfacfpmmul0  22818  lpbl  24459  metustsym  24511  sincosq2sgn  26476  sincosq4sgn  26478  ercgrg  28601  subupgr  29372  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  cplgr3v  29520  pthdivtx  29812  usgr2wlkspthlem1  29842  usgr2wlkspthlem2  29843  wwlknbp  29927  clwlkclwwlklem2a  30085  eleclclwwlknlem2  30148  clwwlknonwwlknonb  30193  clwlknon2num  30455  numclwlk1lem1  30456  numclwlk1lem2  30457  numclwwlk7  30478  frgrreg  30481  shorth  31382  trleile  33063  oddpwdc  34531  bnj1098  34959  bnj999  35133  bnj1118  35159  segcon2  36318  pibt2  37661  lsateln0  39360  cvrcmp2  39649  dalemswapyz  40021  lhprelat3N  40405  cdleme28b  40736  qirropth  43254  onsucf1lem  43615  omlim2  43645  tfsconcatlem  43682  tfsconcatrn  43688  tfsconcatrev  43694  nzin  44663  sigaraf  47200  sigarmf  47201  sigaras  47202  sigarms  47203  sigariz  47210  f1cof1b  47426  afvelrn  47517  elfzelfzlble  47670  prproropf1olem4  47855  prprelprb  47866  fmtnoprmfac2  47916  flsqrt  47942  proththd  47963  evensumeven  48056  evengpop3  48147  evengpoap3  48148  nnsum4primeseven  48149  nnsum4primesevenALTV  48150  tgoldbach  48166  uhgrimisgrgric  48280  gpgedg2ov  48415  gpgedg2iv  48416  lmodvsmdi  48728  ply1mulgsumlem1  48735  lindslinindsimp1  48806  lindsrng01  48817  ldepspr  48822  digexp  48956  dig1  48957  rrx2pnedifcoorneorr  49066  rrxsphere  49097  setrec1lem3  50037