Theorem ancomd 460

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 459	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simprd  494  jccil  521  2reu5  3750  relbrcnvg  6110  soxp  8134  ressuppssdif  8190  relelec  8771  undifixp  8953  funsnfsupp  9417  infmo  9520  fpwwe2lem12  10667  nqpr  11039  infregelb  12231  ssfzunsnext  13581  hashf1rn  14347  hashge2el2dif  14477  pfxccatin12  14719  cshwidxmod  14789  cshweqdif2  14805  pfxco  14825  sinbnd  16160  cosbnd  16161  lcmfun  16619  divgcdcoprmex  16640  cncongr1  16641  vfermltlALT  16774  setsstruct2  17146  funcsetcestrclem8  18156  fullsetcestrc  18160  mgmhmf1o  18663  smndex1iidm  18861  cyccom  19166  rnghmf1o  20403  c0snmgmhm  20413  quscrng  21190  mat1dim0  22419  mat1dimid  22420  mat1dimscm  22421  mat1dimmul  22422  dmatmul  22443  scmatcrng  22467  1marepvsma1  22529  cramerimplem1  22629  cramerimplem2  22630  cpmatacl  22662  cpmatmcllem  22664  decpmatmul  22718  pmatcollpwscmatlem1  22735  chpmat1dlem  22781  chfacfscmul0  22804  chfacfpmmul0  22808  lpbl  24456  metustsym  24508  sincosq2sgn  26479  sincosq4sgn  26481  ercgrg  28393  subupgr  29172  nbgr2vtx1edg  29235  nbuhgr2vtx1edgb  29237  cplgr3v  29320  pthdivtx  29615  usgr2wlkspthlem1  29643  usgr2wlkspthlem2  29644  wwlknbp  29725  clwlkclwwlklem2a  29880  eleclclwwlknlem2  29943  clwwlknonwwlknonb  29988  clwlknon2num  30250  numclwlk1lem1  30251  numclwlk1lem2  30252  numclwwlk7  30273  frgrreg  30276  shorth  31177  trleile  32787  oddpwdc  34105  bnj1098  34545  bnj999  34720  bnj1118  34746  segcon2  35832  pibt2  37027  lsateln0  38597  cvrcmp2  38886  dalemswapyz  39259  lhprelat3N  39643  cdleme28b  39974  qirropth  42470  onsucf1lem  42840  omlim2  42870  tfsconcatlem  42907  tfsconcatrn  42913  tfsconcatrev  42919  nzin  43897  sigaraf  46379  sigarmf  46380  sigaras  46381  sigarms  46382  sigariz  46389  f1cof1b  46595  afvelrn  46686  elfzelfzlble  46839  prproropf1olem4  46983  prprelprb  46994  fmtnoprmfac2  47044  flsqrt  47070  proththd  47091  evensumeven  47184  evengpop3  47275  evengpoap3  47276  nnsum4primeseven  47277  nnsum4primesevenALTV  47278  tgoldbach  47294  lmodvsmdi  47632  ply1mulgsumlem1  47640  lindslinindsimp1  47711  lindsrng01  47722  ldepspr  47727  digexp  47866  dig1  47867  rrx2pnedifcoorneorr  47976  rrxsphere  48007  setrec1lem3  48306