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  3714  relbrcnvg  6061  soxp  8068  ressuppssdif  8124  relelec  8678  undifixp  8867  funsnfsupp  9286  infmo  9391  fpwwe2lem12  10543  nqpr  10915  infregelb  12116  ssfzunsnext  13479  hashf1rn  14269  hashge2el2dif  14397  pfxccatin12  14650  cshwidxmod  14720  cshweqdif2  14736  pfxco  14755  sinbnd  16099  cosbnd  16100  lcmfun  16566  divgcdcoprmex  16587  cncongr1  16588  vfermltlALT  16724  setsstruct2  17095  funcsetcestrclem8  18078  fullsetcestrc  18082  chnccat  18542  mgmhmf1o  18618  smndex1iidm  18819  cyccom  19125  rnghmf1o  20380  c0snmgmhm  20390  quscrng  21230  mat1dim0  22398  mat1dimid  22399  mat1dimscm  22400  mat1dimmul  22401  dmatmul  22422  scmatcrng  22446  1marepvsma1  22508  cramerimplem1  22608  cramerimplem2  22609  cpmatacl  22641  cpmatmcllem  22643  decpmatmul  22697  pmatcollpwscmatlem1  22714  chpmat1dlem  22760  chfacfscmul0  22783  chfacfpmmul0  22787  lpbl  24428  metustsym  24480  sincosq2sgn  26445  sincosq4sgn  26447  ercgrg  28505  subupgr  29276  nbgr2vtx1edg  29339  nbuhgr2vtx1edgb  29341  cplgr3v  29424  pthdivtx  29716  usgr2wlkspthlem1  29746  usgr2wlkspthlem2  29747  wwlknbp  29831  clwlkclwwlklem2a  29989  eleclclwwlknlem2  30052  clwwlknonwwlknonb  30097  clwlknon2num  30359  numclwlk1lem1  30360  numclwlk1lem2  30361  numclwwlk7  30382  frgrreg  30385  shorth  31286  trleile  32963  oddpwdc  34378  bnj1098  34806  bnj999  34981  bnj1118  35007  segcon2  36160  pibt2  37472  lsateln0  39104  cvrcmp2  39393  dalemswapyz  39765  lhprelat3N  40149  cdleme28b  40480  qirropth  43015  onsucf1lem  43376  omlim2  43406  tfsconcatlem  43443  tfsconcatrn  43449  tfsconcatrev  43455  nzin  44425  sigaraf  46965  sigarmf  46966  sigaras  46967  sigarms  46968  sigariz  46975  f1cof1b  47191  afvelrn  47282  elfzelfzlble  47435  prproropf1olem4  47620  prprelprb  47631  fmtnoprmfac2  47681  flsqrt  47707  proththd  47728  evensumeven  47821  evengpop3  47912  evengpoap3  47913  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  tgoldbach  47931  uhgrimisgrgric  48045  gpgedg2ov  48180  gpgedg2iv  48181  lmodvsmdi  48493  ply1mulgsumlem1  48501  lindslinindsimp1  48572  lindsrng01  48583  ldepspr  48588  digexp  48722  dig1  48723  rrx2pnedifcoorneorr  48832  rrxsphere  48863  setrec1lem3  49804