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  6071  soxp  8079  ressuppssdif  8135  relelec  8691  undifixp  8882  funsnfsupp  9305  infmo  9410  fpwwe2lem12  10565  nqpr  10937  infregelb  12140  ssfzunsnext  13523  hashf1rn  14314  hashge2el2dif  14442  pfxccatin12  14695  cshwidxmod  14765  cshweqdif2  14781  pfxco  14800  sinbnd  16147  cosbnd  16148  lcmfun  16614  divgcdcoprmex  16635  cncongr1  16636  vfermltlALT  16773  setsstruct2  17144  funcsetcestrclem8  18128  fullsetcestrc  18132  chnccat  18592  mgmhmf1o  18668  smndex1iidm  18869  cyccom  19178  rnghmf1o  20432  c0snmgmhm  20442  quscrng  21281  mat1dim0  22438  mat1dimid  22439  mat1dimscm  22440  mat1dimmul  22441  dmatmul  22462  scmatcrng  22486  1marepvsma1  22548  cramerimplem1  22648  cramerimplem2  22649  cpmatacl  22681  cpmatmcllem  22683  decpmatmul  22737  pmatcollpwscmatlem1  22754  chpmat1dlem  22800  chfacfscmul0  22823  chfacfpmmul0  22827  lpbl  24468  metustsym  24520  sincosq2sgn  26463  sincosq4sgn  26465  ercgrg  28585  subupgr  29356  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  cplgr3v  29504  pthdivtx  29795  usgr2wlkspthlem1  29825  usgr2wlkspthlem2  29826  wwlknbp  29910  clwlkclwwlklem2a  30068  eleclclwwlknlem2  30131  clwwlknonwwlknonb  30176  clwlknon2num  30438  numclwlk1lem1  30439  numclwlk1lem2  30440  numclwwlk7  30461  frgrreg  30464  shorth  31366  trleile  33031  oddpwdc  34498  bnj1098  34926  bnj999  35100  bnj1118  35126  segcon2  36287  pibt2  37733  lsateln0  39441  cvrcmp2  39730  dalemswapyz  40102  lhprelat3N  40486  cdleme28b  40817  qirropth  43336  onsucf1lem  43697  omlim2  43727  tfsconcatlem  43764  tfsconcatrn  43770  tfsconcatrev  43776  nzin  44745  sigaraf  47281  sigarmf  47282  sigaras  47283  sigarms  47284  sigariz  47291  f1cof1b  47519  afvelrn  47610  elfzelfzlble  47763  prproropf1olem4  47960  prprelprb  47971  fmtnoprmfac2  48024  flsqrt  48050  proththd  48071  evensumeven  48177  evengpop3  48268  evengpoap3  48269  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  tgoldbach  48287  uhgrimisgrgric  48401  gpgedg2ov  48536  gpgedg2iv  48537  lmodvsmdi  48849  ply1mulgsumlem1  48856  lindslinindsimp1  48927  lindsrng01  48938  ldepspr  48943  digexp  49077  dig1  49078  rrx2pnedifcoorneorr  49187  rrxsphere  49218  setrec1lem3  50158