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  3715  relbrcnvg  6051  soxp  8054  ressuppssdif  8110  relelec  8664  undifixp  8853  funsnfsupp  9271  infmo  9376  fpwwe2lem12  10525  nqpr  10897  infregelb  12098  ssfzunsnext  13461  hashf1rn  14251  hashge2el2dif  14379  pfxccatin12  14632  cshwidxmod  14702  cshweqdif2  14718  pfxco  14737  sinbnd  16081  cosbnd  16082  lcmfun  16548  divgcdcoprmex  16569  cncongr1  16570  vfermltlALT  16706  setsstruct2  17077  funcsetcestrclem8  18060  fullsetcestrc  18064  chnccat  18524  mgmhmf1o  18600  smndex1iidm  18801  cyccom  19108  rnghmf1o  20363  c0snmgmhm  20373  quscrng  21213  mat1dim0  22381  mat1dimid  22382  mat1dimscm  22383  mat1dimmul  22384  dmatmul  22405  scmatcrng  22429  1marepvsma1  22491  cramerimplem1  22591  cramerimplem2  22592  cpmatacl  22624  cpmatmcllem  22626  decpmatmul  22680  pmatcollpwscmatlem1  22697  chpmat1dlem  22743  chfacfscmul0  22766  chfacfpmmul0  22770  lpbl  24411  metustsym  24463  sincosq2sgn  26428  sincosq4sgn  26430  ercgrg  28488  subupgr  29258  nbgr2vtx1edg  29321  nbuhgr2vtx1edgb  29323  cplgr3v  29406  pthdivtx  29698  usgr2wlkspthlem1  29728  usgr2wlkspthlem2  29729  wwlknbp  29813  clwlkclwwlklem2a  29968  eleclclwwlknlem2  30031  clwwlknonwwlknonb  30076  clwlknon2num  30338  numclwlk1lem1  30339  numclwlk1lem2  30340  numclwwlk7  30361  frgrreg  30364  shorth  31265  trleile  32942  oddpwdc  34357  bnj1098  34785  bnj999  34960  bnj1118  34986  segcon2  36118  pibt2  37430  lsateln0  39013  cvrcmp2  39302  dalemswapyz  39674  lhprelat3N  40058  cdleme28b  40389  qirropth  42920  onsucf1lem  43281  omlim2  43311  tfsconcatlem  43348  tfsconcatrn  43354  tfsconcatrev  43360  nzin  44330  sigaraf  46870  sigarmf  46871  sigaras  46872  sigarms  46873  sigariz  46880  f1cof1b  47087  afvelrn  47178  elfzelfzlble  47331  prproropf1olem4  47516  prprelprb  47527  fmtnoprmfac2  47577  flsqrt  47603  proththd  47624  evensumeven  47717  evengpop3  47808  evengpoap3  47809  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  tgoldbach  47827  uhgrimisgrgric  47941  gpgedg2ov  48076  gpgedg2iv  48077  lmodvsmdi  48389  ply1mulgsumlem1  48397  lindslinindsimp1  48468  lindsrng01  48479  ldepspr  48484  digexp  48618  dig1  48619  rrx2pnedifcoorneorr  48728  rrxsphere  48759  setrec1lem3  49700