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  3720  relbrcnvg  6060  soxp  8069  ressuppssdif  8125  relelec  8679  undifixp  8868  funsnfsupp  9301  infmo  9406  fpwwe2lem12  10555  nqpr  10927  infregelb  12127  ssfzunsnext  13490  hashf1rn  14277  hashge2el2dif  14405  pfxccatin12  14657  cshwidxmod  14727  cshweqdif2  14743  pfxco  14763  sinbnd  16107  cosbnd  16108  lcmfun  16574  divgcdcoprmex  16595  cncongr1  16596  vfermltlALT  16732  setsstruct2  17103  funcsetcestrclem8  18086  fullsetcestrc  18090  mgmhmf1o  18592  smndex1iidm  18793  cyccom  19100  rnghmf1o  20355  c0snmgmhm  20365  quscrng  21208  mat1dim0  22376  mat1dimid  22377  mat1dimscm  22378  mat1dimmul  22379  dmatmul  22400  scmatcrng  22424  1marepvsma1  22486  cramerimplem1  22586  cramerimplem2  22587  cpmatacl  22619  cpmatmcllem  22621  decpmatmul  22675  pmatcollpwscmatlem1  22692  chpmat1dlem  22738  chfacfscmul0  22761  chfacfpmmul0  22765  lpbl  24407  metustsym  24459  sincosq2sgn  26424  sincosq4sgn  26426  ercgrg  28480  subupgr  29250  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  cplgr3v  29398  pthdivtx  29690  usgr2wlkspthlem1  29720  usgr2wlkspthlem2  29721  wwlknbp  29805  clwlkclwwlklem2a  29960  eleclclwwlknlem2  30023  clwwlknonwwlknonb  30068  clwlknon2num  30330  numclwlk1lem1  30331  numclwlk1lem2  30332  numclwwlk7  30353  frgrreg  30356  shorth  31257  trleile  32926  oddpwdc  34321  bnj1098  34749  bnj999  34924  bnj1118  34950  segcon2  36078  pibt2  37390  lsateln0  38973  cvrcmp2  39262  dalemswapyz  39635  lhprelat3N  40019  cdleme28b  40350  qirropth  42881  onsucf1lem  43242  omlim2  43272  tfsconcatlem  43309  tfsconcatrn  43315  tfsconcatrev  43321  nzin  44291  sigaraf  46835  sigarmf  46836  sigaras  46837  sigarms  46838  sigariz  46845  f1cof1b  47062  afvelrn  47153  elfzelfzlble  47306  prproropf1olem4  47491  prprelprb  47502  fmtnoprmfac2  47552  flsqrt  47578  proththd  47599  evensumeven  47692  evengpop3  47783  evengpoap3  47784  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  tgoldbach  47802  uhgrimisgrgric  47915  gpgedg2ov  48041  gpgedg2iv  48042  lmodvsmdi  48351  ply1mulgsumlem1  48359  lindslinindsimp1  48430  lindsrng01  48441  ldepspr  48446  digexp  48580  dig1  48581  rrx2pnedifcoorneorr  48690  rrxsphere  48721  setrec1lem3  49662