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  3729  relbrcnvg  6076  soxp  8108  ressuppssdif  8164  relelec  8718  undifixp  8907  funsnfsupp  9343  infmo  9448  fpwwe2lem12  10595  nqpr  10967  infregelb  12167  ssfzunsnext  13530  hashf1rn  14317  hashge2el2dif  14445  pfxccatin12  14698  cshwidxmod  14768  cshweqdif2  14784  pfxco  14804  sinbnd  16148  cosbnd  16149  lcmfun  16615  divgcdcoprmex  16636  cncongr1  16637  vfermltlALT  16773  setsstruct2  17144  funcsetcestrclem8  18123  fullsetcestrc  18127  mgmhmf1o  18627  smndex1iidm  18828  cyccom  19135  rnghmf1o  20361  c0snmgmhm  20371  quscrng  21193  mat1dim0  22360  mat1dimid  22361  mat1dimscm  22362  mat1dimmul  22363  dmatmul  22384  scmatcrng  22408  1marepvsma1  22470  cramerimplem1  22570  cramerimplem2  22571  cpmatacl  22603  cpmatmcllem  22605  decpmatmul  22659  pmatcollpwscmatlem1  22676  chpmat1dlem  22722  chfacfscmul0  22745  chfacfpmmul0  22749  lpbl  24391  metustsym  24443  sincosq2sgn  26408  sincosq4sgn  26410  ercgrg  28444  subupgr  29214  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  cplgr3v  29362  pthdivtx  29657  usgr2wlkspthlem1  29687  usgr2wlkspthlem2  29688  wwlknbp  29772  clwlkclwwlklem2a  29927  eleclclwwlknlem2  29990  clwwlknonwwlknonb  30035  clwlknon2num  30297  numclwlk1lem1  30298  numclwlk1lem2  30299  numclwwlk7  30320  frgrreg  30323  shorth  31224  trleile  32897  oddpwdc  34345  bnj1098  34773  bnj999  34948  bnj1118  34974  segcon2  36093  pibt2  37405  lsateln0  38988  cvrcmp2  39277  dalemswapyz  39650  lhprelat3N  40034  cdleme28b  40365  qirropth  42896  onsucf1lem  43258  omlim2  43288  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcatrev  43337  nzin  44307  sigaraf  46851  sigarmf  46852  sigaras  46853  sigarms  46854  sigariz  46861  f1cof1b  47078  afvelrn  47169  elfzelfzlble  47322  prproropf1olem4  47507  prprelprb  47518  fmtnoprmfac2  47568  flsqrt  47594  proththd  47615  evensumeven  47708  evengpop3  47799  evengpoap3  47800  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  tgoldbach  47818  uhgrimisgrgric  47931  gpgedg2ov  48057  gpgedg2iv  48058  lmodvsmdi  48367  ply1mulgsumlem1  48375  lindslinindsimp1  48446  lindsrng01  48457  ldepspr  48462  digexp  48596  dig1  48597  rrx2pnedifcoorneorr  48706  rrxsphere  48737  setrec1lem3  49678