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  3705  relbrcnvg  6062  soxp  8070  ressuppssdif  8126  relelec  8682  undifixp  8873  funsnfsupp  9296  infmo  9401  fpwwe2lem12  10554  nqpr  10926  infregelb  12129  ssfzunsnext  13512  hashf1rn  14303  hashge2el2dif  14431  pfxccatin12  14684  cshwidxmod  14754  cshweqdif2  14770  pfxco  14789  sinbnd  16136  cosbnd  16137  lcmfun  16603  divgcdcoprmex  16624  cncongr1  16625  vfermltlALT  16762  setsstruct2  17133  funcsetcestrclem8  18117  fullsetcestrc  18121  chnccat  18581  mgmhmf1o  18657  smndex1iidm  18858  cyccom  19167  rnghmf1o  20421  c0snmgmhm  20431  quscrng  21271  mat1dim0  22447  mat1dimid  22448  mat1dimscm  22449  mat1dimmul  22450  dmatmul  22471  scmatcrng  22495  1marepvsma1  22557  cramerimplem1  22657  cramerimplem2  22658  cpmatacl  22690  cpmatmcllem  22692  decpmatmul  22746  pmatcollpwscmatlem1  22763  chpmat1dlem  22809  chfacfscmul0  22832  chfacfpmmul0  22836  lpbl  24477  metustsym  24529  sincosq2sgn  26479  sincosq4sgn  26481  ercgrg  28604  subupgr  29375  nbgr2vtx1edg  29438  nbuhgr2vtx1edgb  29440  cplgr3v  29523  pthdivtx  29815  usgr2wlkspthlem1  29845  usgr2wlkspthlem2  29846  wwlknbp  29930  clwlkclwwlklem2a  30088  eleclclwwlknlem2  30151  clwwlknonwwlknonb  30196  clwlknon2num  30458  numclwlk1lem1  30459  numclwlk1lem2  30460  numclwwlk7  30481  frgrreg  30484  shorth  31386  trleile  33051  oddpwdc  34519  bnj1098  34947  bnj999  35121  bnj1118  35147  segcon2  36308  pibt2  37744  lsateln0  39452  cvrcmp2  39741  dalemswapyz  40113  lhprelat3N  40497  cdleme28b  40828  qirropth  43351  onsucf1lem  43712  omlim2  43742  tfsconcatlem  43779  tfsconcatrn  43785  tfsconcatrev  43791  nzin  44760  sigaraf  47296  sigarmf  47297  sigaras  47298  sigarms  47299  sigariz  47306  f1cof1b  47522  afvelrn  47613  elfzelfzlble  47766  prproropf1olem4  47963  prprelprb  47974  fmtnoprmfac2  48027  flsqrt  48053  proththd  48074  evensumeven  48180  evengpop3  48271  evengpoap3  48272  nnsum4primeseven  48273  nnsum4primesevenALTV  48274  tgoldbach  48290  uhgrimisgrgric  48404  gpgedg2ov  48539  gpgedg2iv  48540  lmodvsmdi  48852  ply1mulgsumlem1  48859  lindslinindsimp1  48930  lindsrng01  48941  ldepspr  48946  digexp  49080  dig1  49081  rrx2pnedifcoorneorr  49190  rrxsphere  49221  setrec1lem3  50161