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  3732  relbrcnvg  6079  soxp  8111  ressuppssdif  8167  relelec  8721  undifixp  8910  funsnfsupp  9350  infmo  9455  fpwwe2lem12  10602  nqpr  10974  infregelb  12174  ssfzunsnext  13537  hashf1rn  14324  hashge2el2dif  14452  pfxccatin12  14705  cshwidxmod  14775  cshweqdif2  14791  pfxco  14811  sinbnd  16155  cosbnd  16156  lcmfun  16622  divgcdcoprmex  16643  cncongr1  16644  vfermltlALT  16780  setsstruct2  17151  funcsetcestrclem8  18130  fullsetcestrc  18134  mgmhmf1o  18634  smndex1iidm  18835  cyccom  19142  rnghmf1o  20368  c0snmgmhm  20378  quscrng  21200  mat1dim0  22367  mat1dimid  22368  mat1dimscm  22369  mat1dimmul  22370  dmatmul  22391  scmatcrng  22415  1marepvsma1  22477  cramerimplem1  22577  cramerimplem2  22578  cpmatacl  22610  cpmatmcllem  22612  decpmatmul  22666  pmatcollpwscmatlem1  22683  chpmat1dlem  22729  chfacfscmul0  22752  chfacfpmmul0  22756  lpbl  24398  metustsym  24450  sincosq2sgn  26415  sincosq4sgn  26417  ercgrg  28451  subupgr  29221  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  cplgr3v  29369  pthdivtx  29664  usgr2wlkspthlem1  29694  usgr2wlkspthlem2  29695  wwlknbp  29779  clwlkclwwlklem2a  29934  eleclclwwlknlem2  29997  clwwlknonwwlknonb  30042  clwlknon2num  30304  numclwlk1lem1  30305  numclwlk1lem2  30306  numclwwlk7  30327  frgrreg  30330  shorth  31231  trleile  32904  oddpwdc  34352  bnj1098  34780  bnj999  34955  bnj1118  34981  segcon2  36100  pibt2  37412  lsateln0  38995  cvrcmp2  39284  dalemswapyz  39657  lhprelat3N  40041  cdleme28b  40372  qirropth  42903  onsucf1lem  43265  omlim2  43295  tfsconcatlem  43332  tfsconcatrn  43338  tfsconcatrev  43344  nzin  44314  sigaraf  46858  sigarmf  46859  sigaras  46860  sigarms  46861  sigariz  46868  f1cof1b  47082  afvelrn  47173  elfzelfzlble  47326  prproropf1olem4  47511  prprelprb  47522  fmtnoprmfac2  47572  flsqrt  47598  proththd  47619  evensumeven  47712  evengpop3  47803  evengpoap3  47804  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  tgoldbach  47822  uhgrimisgrgric  47935  gpgedg2ov  48061  gpgedg2iv  48062  lmodvsmdi  48371  ply1mulgsumlem1  48379  lindslinindsimp1  48450  lindsrng01  48461  ldepspr  48466  digexp  48600  dig1  48601  rrx2pnedifcoorneorr  48710  rrxsphere  48741  setrec1lem3  49682