Theorem syl6eq 2872

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
syl6eq.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eq.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6eq	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl6eq

Step	Hyp	Ref	Expression
1		syl6eq.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eq.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2856	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  syl6req  2873  syl6eqr  2874  3eqtr3g  2879  3eqtr4a  2882  cbvrabcsfw  3924  cbvralcsf  3925  cbvreucsf  3927  cbvrabcsf  3928  un00  4394  disjeq0  4405  disjpr2  4649  tppreq3  4695  ssprsseq  4758  preq12b  4781  prnebg  4786  preq12nebg  4793  elpr2elpr  4799  opidg  4822  intsng  4911  uniintsn  4913  rint0  4916  iinrab2  4992  riin0  5004  iunxdif3  5017  iununi  5021  disjprgw  5061  disjprg  5062  disjxun  5064  intex  5240  intnex  5241  2rbropap  5451  xpriindi  5707  dmxpid  5800  elreldm  5805  relimasn  5952  elimasni  5956  inisegn0  5961  xpnz  6016  dmxpss  6028  rnxpid  6030  xpcan  6033  xpcan2  6034  xpima  6039  csbrn  6060  dmsnopss  6071  opswap  6086  unixp  6133  unixp0  6134  unixpid  6135  xpcoid  6141  uniabio  6328  iotanul  6333  cnvresid  6433  funimacnv  6435  resasplit  6548  fimadmfo  6599  f1o00  6649  f1oprswap  6658  rnfvprc  6664  dffv3  6666  fv2prc  6710  fnrnfv  6725  feqresmpt  6734  funfv  6750  funfv2f  6752  fvun1  6754  dffv2  6756  fvmpt2f  6769  fvmpt2i  6778  fndmin  6815  fniniseg2  6832  fveqressseq  6847  fmptcof  6892  fmptcos  6893  funiun  6909  funopsn  6910  funopdmsn  6912  funsneqopb  6914  fvunsn  6941  fvpr1  6952  fconst5  6968  resfunexg  6978  csbov123  7198  fnrnov  7321  2mpo0  7394  elovmpt3imp  7402  offval  7416  ofrfval  7417  onuninsuci  7555  1stval  7691  2ndval  7692  1stnpr  7693  2ndnpr  7694  op1std  7699  op2ndd  7700  1st2val  7717  2nd2val  7718  2nd1st  7737  offval22  7783  bropopvvv  7785  bropfvvvvlem  7786  fmpoco  7790  cnvf1olem  7805  fparlem3  7809  fparlem4  7810  offsplitfpar  7815  suppsnop  7844  mptsuppdifd  7852  suppco  7870  supp0cosupp0  7872  supp0cosupp0OLD  7873  tpostpos  7912  mpocurryvald  7936  tfrlem11  8024  tfrlem16  8029  tfr2b  8032  tz7.44-1  8042  tz7.44-2  8043  tz7.44-3  8044  2oconcl  8128  om0  8142  oe0m  8143  oe0  8147  oev2  8148  om0r  8164  oe1m  8171  oawordeulem  8180  oa00  8185  oarec  8188  oacomf1o  8191  oeworde  8219  oeoa  8223  oeoelem  8224  oeoe  8225  nnm0r  8236  nneob  8279  ecexr  8294  uniqs2  8359  mapsnconst  8456  undifixp  8498  en1  8576  en1b  8577  fundmen  8583  xpsnen  8601  xpcomco  8607  xpdom2  8612  sbthlem5  8631  sbthlem8  8634  fodomr  8668  domss2  8676  xpmapenlem  8684  domunfican  8791  fiint  8795  fodomfi  8797  iunfi  8812  pwfi  8819  fsuppmptif  8863  elfi2  8878  fi0  8884  fieq0  8885  fisn  8891  elfiun  8894  dffi3  8895  marypha1lem  8897  marypha2lem3  8901  supval2  8919  supsn  8936  infltoreq  8966  infsn  8969  oicl  8993  oif  8994  hartogslem1  9006  wemaplem2  9011  inf3lema  9087  inf3lemd  9090  infdiffi  9121  cantnfdm  9127  cantnfvalf  9128  cantnfval2  9132  cantnflt  9135  cantnf0  9138  cantnfp1lem3  9143  cantnflem1  9152  cantnf  9156  tc00  9190  r1tr  9205  r1pwss  9213  r1val1  9215  rankval2  9247  rankeq0b  9289  rankxplim3  9310  scott0  9315  oncard  9389  cardnueq0  9393  cardmin2  9427  pm54.43lem  9428  en2other2  9435  fseqenlem1  9450  fseqenlem2  9451  dfac8alem  9455  acndom  9477  alephnbtwn  9497  cardaleph  9515  iunfictbso  9540  dfac5lem3  9551  dfac9  9562  kmlem2  9577  kmlem11  9586  ackbij1lem1  9642  ackbij1lem8  9649  ackbij2lem2  9662  r1om  9666  cardcf  9674  cfeq0  9678  cfval2  9682  cflim2  9685  cfsmolem  9692  fin23lem26  9747  fin23lem30  9764  isf34lem6  9802  fin1a2lem10  9831  fin1a2lem11  9832  itunisuc  9841  ituniiun  9844  hsmex  9854  axdc3lem4  9875  axdc4lem  9877  zorn2lem1  9918  ttukeylem4  9934  alephadd  9999  pwcfsdom  10005  cfpwsdom  10006  alephom  10007  fpwwe2lem13  10064  pwfseqlem1  10080  winalim2  10118  r1wunlim  10159  rankcf  10199  r1tskina  10204  gruf  10233  grur1a  10241  sstskm  10264  recmulnq  10386  genpv  10421  addcompr  10443  mulcompr  10445  distrlem1pr  10447  mulcmpblnrlem  10492  recexsrlem  10525  addresr  10560  mulresr  10561  axcnre  10586  00id  10815  mul02  10818  cnegex  10821  add20  11152  msqge0  11161  recextlem2  11271  fv0p1e1  11761  div4p1lem1div2  11893  nnm1nn0  11939  frnnn0supp  11954  znegcl  12018  nneo  12067  nn0ind-raph  12083  xrmaxeq  12573  xnegneg  12608  xltnegi  12610  xaddpnf1  12620  xaddmnf1  12622  xnegid  12632  xnn0xadd0  12641  xnegdi  12642  xsubge0  12655  xlesubadd  12657  xmul01  12661  xmulneg1  12663  xmulmnf1  12670  xlemul1a  12682  xadddilem  12688  fz0to4untppr  13011  fz0sn0fz1  13025  fzo0to2pr  13123  fldiv4p1lem1div2  13206  fldiv4lem1div2  13208  mulp1mod1  13281  om2uzrdg  13325  uzrdgsuci  13329  fzennn  13337  seqof2  13429  exp0  13434  exp1  13436  expp1  13437  expneg  13438  1exp  13459  mulexp  13469  m1expeven  13477  sq0i  13557  bernneq  13591  discr1  13601  discr  13602  facp1  13639  faclbnd3  13653  faclbnd4lem1  13654  faclbnd4lem3  13656  faclbnd4lem4  13657  facubnd  13661  bcval5  13679  hashsng  13731  hashrabsn01  13735  hashsn01  13778  hash1snb  13781  hashxplem  13795  hashpw  13798  hashfun  13799  resunimafz0  13804  hashbclem  13811  hashbc  13812  hashf1lem2  13815  hashf1  13816  fz1isolem  13820  hash2prde  13829  hash2pwpr  13835  wrdnfi  13899  lsw1  13919  s1rn  13953  s1dm  13962  eqs1  13966  ccatws1len  13974  ccat2s1len  13977  ccat2s1lenOLD  13978  ccat1st1st  13984  swrd00  14006  swrdlend  14015  swrds1  14028  pfx00  14036  pfx0  14037  repswsymballbi  14142  cshword  14153  cshwmodn  14157  cshw1  14184  ccatco  14197  s2dm  14252  wrdlen2s2  14307  wrdl2exs2  14308  pfx2  14309  wrdlen3s3  14311  wwlktovf1  14321  eqwrds3  14325  ofccat  14329  dmtrclfv  14378  relexpsucr  14388  relexpsucnnl  14391  relexpsucl  14392  relexpdmg  14401  relexprng  14405  relexpfld  14408  relexpaddnn  14410  relexpaddg  14412  shftdm  14430  imre  14467  reim0b  14478  rereb  14479  sqeqd  14525  cnpart  14599  sqr0lem  14600  sqrmo  14611  abs00  14649  max0add  14670  abs1m  14695  cnsqrt00  14752  climconst  14900  rlimconst  14901  lo1resb  14921  rlimresb  14922  o1resb  14923  isercolllem3  15023  iseraltlem2  15039  iseraltlem3  15040  fsum  15077  sumz  15079  fsumf1o  15080  sumss  15081  fsumcllem  15089  fsumsplitf  15098  fsumxp  15127  fsumcnv  15128  fsumshftm  15136  fsummulc2  15139  fsumconst  15145  fsumabs  15156  telfsumo  15157  fsumparts  15161  fsumrelem  15162  fsumrlim  15166  fsumo1  15167  fsumiun  15176  binomlem  15184  binom  15185  binom11  15187  incexclem  15191  incexc  15192  isumsplit  15195  climcndslem1  15204  climcndslem2  15205  arisum  15215  arisum2  15216  trireciplem  15217  pwdif  15223  pwm1geoserOLD  15225  geolim  15226  geolim2  15227  georeclim  15228  geomulcvg  15232  geoisumr  15234  prodfrec  15251  fprod  15295  prod1  15298  fprodf1o  15300  fprodcllem  15305  fproddiv  15315  fprodfac  15327  fprodconst  15332  fprodn0  15333  fprod2d  15335  fprodxp  15336  fprodcnv  15337  fprodmodd  15351  risefac0  15381  fallfac0  15382  0fallfac  15391  binomfallfac  15395  fallfacfac  15399  bpolylem  15402  bpoly0  15404  bpoly1  15405  bpolysum  15407  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  ef0lem  15432  ege2le3  15443  efaddlem  15446  efcan  15449  efsep  15463  eft0val  15465  ef4p  15466  efi4p  15490  sincossq  15529  cos2tsin  15532  absefi  15549  demoivreALT  15554  ruclem4  15587  ruclem8  15590  ruclem11  15593  ruclem13  15595  p1modz1  15614  dvdsabseq  15663  odd2np1lem  15689  oddp1even  15693  mod2eq1n2dvds  15696  opoe  15712  m1expo  15726  m1exp1  15727  nn0o1gt2  15732  sumodd  15739  pwp1fsum  15742  divalglem8  15751  bitsinv1  15791  bitsf1ocnv  15793  bitsinvp1  15798  sadcaddlem  15806  sadcadd  15807  sadadd2  15809  sadid1  15817  bitsres  15822  smupp1  15829  smuval2  15831  smumullem  15841  gcddvds  15852  gcdcl  15855  gcdeq0  15865  gcd0id  15867  gcdaddmlem  15872  bezoutr1  15913  seq1st  15915  eucalglt  15929  eucalg  15931  lcm0val  15938  lcmid  15953  lcmfun  15989  lcmf2a3a4e12  15991  rpmul  16003  2mulprm  16037  dfphi2  16111  phiprmpw  16113  hashgcdeq  16126  odzdvds  16132  nnnn0modprm0  16143  pythagtriplem4  16156  pythagtriplem12  16163  pcaddlem  16224  pcmpt  16228  pockthi  16243  prmreclem1  16252  prmreclem2  16253  prmreclem4  16255  prmreclem5  16256  4sqlem12  16292  vdwapval  16309  vdwap1  16313  vdwlem8  16324  vdwlem13  16329  hashbc0  16341  ramcl2lem  16345  ramub2  16350  ramz2  16360  ramcl  16365  prmodvdslcmf  16383  2expltfac  16426  cshws0  16435  prmlem0  16439  setsdm  16517  setsres  16525  ressval3d  16561  strle1  16592  0rest  16703  restid2  16704  firest  16706  prdsbas3  16754  mrcun  16893  mreexmrid  16914  mreexexlem3d  16917  oppcco  16987  oppccomfpropd  16997  dfiso2  17042  sscfn1  17087  sscfn2  17088  rescval2  17098  idfu2nd  17147  idfu1st  17149  idfucl  17151  cofuval  17152  cofu1st  17153  cofu2nd  17155  cofucl  17158  resfval2  17163  resf1st  17164  fuchom  17231  homarcl  17288  arwval  17303  ida2  17319  coafval  17324  coa2  17329  setcepi  17348  estrres  17389  xpccatid  17438  1stfval  17441  2ndfval  17444  prf1st  17454  prf2nd  17455  curf1cl  17478  curf2cl  17481  curfcl  17482  uncfcurf  17489  curf2ndf  17497  hofcl  17509  yon11  17514  yonedalem4c  17527  yonedalem3b  17529  yonedalem3  17530  lubdm  17589  glbdm  17602  joinfval2  17612  joindm  17613  meetfval2  17626  meetdm  17627  oduleval  17741  odumeet  17750  odujoin  17752  posglbd  17760  cnvps  17822  gsumwsubmcl  18001  gsumccatOLD  18005  gsumccat  18006  gsumwmhm  18010  frmdplusg  18019  frmdgsum  18027  frmdup1  18029  efmndtopn  18048  efmnd1hash  18057  efmnd2hash  18059  smndex1gid  18068  smndex1igid  18069  smndex1mgm  18072  smndex1n0mnd  18077  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  pwmndid  18101  pwmnd  18102  grplactcnv  18202  mulgfval  18226  mulgfvalALT  18227  mulgfvi  18230  mulg0  18231  mulgnn0gsum  18234  mulgneg  18246  mulgneg2  18261  gaid  18429  cntzrcl  18457  cntziinsn  18465  gsumwrev  18494  symgval  18497  symgplusg  18511  symg1hash  18518  symg2hash  18520  symg2bas  18521  galactghm  18532  symgtopn  18534  gsmsymgrfix  18556  pmtrprfval  18615  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem4  18625  psgnfval  18628  psgnpmtr  18638  psgnprfval1  18650  odfval  18660  odfvalALT  18661  odval  18662  sylow1lem2  18724  sylow2a  18744  sylow3lem1  18752  oppglsm  18767  efgval  18843  efgtlen  18852  efginvrel2  18853  efgsval2  18859  efgs1  18861  efgs1b  18862  efgsp1  18863  efgredlema  18866  efgrelexlema  18875  efgredeu  18878  frgpuptinv  18897  odadd1  18968  odadd  18970  prmcyg  19014  lt6abl  19015  gsumval3  19027  gsumcllem  19028  gsumzres  19029  gsumzaddlem  19041  gsummptfzsplitl  19053  gsumconst  19054  gsum2dlem2  19091  gsum2d2  19094  gsumcom2  19095  gsumxp  19096  dprdsn  19158  dmdprdsplitlem  19159  dprd2da  19164  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dpjidcl  19180  ablfac1eulem  19194  ablfac1eu  19195  pgpfaclem1  19203  srgbinom  19295  ringpropd  19332  crngpropd  19333  isringd  19335  iscrngd  19336  gsumdixp  19359  invrfval  19423  rngidpropd  19445  unitpropd  19447  invrpropd  19448  isdrngrd  19528  subrgpropd  19570  rhmpropd  19571  srngmul  19629  lspuni0  19782  pwssplit1  19831  lbspropd  19871  lbsextlem4  19933  lidlrsppropd  20003  rrgval  20060  assamulgscmlem2  20129  psrbagaddcl  20150  psrbaglefi  20152  psrplusg  20161  psrvscafval  20170  mvrid  20203  mplsca  20225  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  ltbwe  20253  opsrle  20256  opsrtoslem1  20264  evlslem2  20292  mpfrcl  20298  selvval  20331  ply1sca  20421  coe1z  20431  coe1mul2lem1  20435  coe1mul2lem2  20436  coe1fzgsumdlem  20469  gsumply1eq  20473  lply1binomsc  20475  ply1frcl  20481  evls1sca  20486  evl1fval1lem  20493  evl1gsumdlem  20519  xrsdsreclblem  20591  gzrngunit  20611  gsumfsum  20612  zringunit  20635  zrhval  20655  zrhval2  20656  chrval  20672  evpmodpmf1o  20740  psgndiflemA  20745  elocv  20812  ocvz  20822  pjfval  20850  obsipid  20866  dsmmfi  20882  frlmsca  20897  mamulid  21050  mamurid  21051  ofco2  21060  mattposvs  21064  mattpos1  21065  mat1dim0  21082  mat1dimid  21083  mat1dimscm  21084  scmatf1  21140  mavmul0  21161  mavmul0g  21162  nfimdetndef  21198  mdetfval1  21199  mdet0pr  21201  mdet0fv0  21203  mdetdiagid  21209  mdetralt  21217  mdetralt2  21218  mdetunilem9  21229  m2detleiblem1  21233  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  madufval  21246  maducoeval2  21249  madurid  21253  cramer0  21299  mat2pmatfval  21331  d0mat2pmat  21346  decpmatval  21373  pmatcollpw3lem  21391  pmatcollpw3fi1lem1  21394  pmatcollpwscmatlem1  21397  mp2pm2mplem3  21416  chmatval  21437  chpmat0d  21442  chpdmatlem3  21448  chpscmatgsumbin  21452  chpidmat  21455  chfacffsupp  21464  cayleyhamilton1  21500  tgval2  21564  tgidm  21588  indistopon  21609  fctop  21612  cctop  21614  epttop  21617  indiscld  21699  mretopd  21700  tgrest  21767  restco  21772  restsn  21778  restcld  21780  ordtbaslem  21796  ordtbas2  21799  ordtcnv  21809  lecldbas  21827  iscnp2  21847  tgcn  21860  cnpresti  21896  cnprest  21897  cnindis  21900  cnhaus  21962  ordthauslem  21991  cmpsublem  22007  fiuncmp  22012  hauscmplem  22014  cmpfi  22016  conndisj  22024  dfconn2  22027  islocfin  22125  dissnref  22136  dissnlocfin  22137  comppfsc  22140  txbas  22175  ptbasin  22185  ptbasfi  22189  dfac14lem  22225  dfac14  22226  xkoccn  22227  upxp  22231  uptx  22233  txrest  22239  txdis  22240  txindislem  22241  txtube  22248  txcmplem1  22249  txcmplem2  22250  txkgen  22260  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  xkofvcn  22292  xkoinjcn  22295  txhmeo  22411  txswaphmeolem  22412  ptuncnv  22415  ptcmpfi  22421  fbssint  22446  fbun  22448  snfil  22472  filconn  22491  csdfil  22502  filufint  22528  ufinffr  22537  lmflf  22613  fclscmpi  22637  fclscmp  22638  alexsublem  22652  alexsubALTlem2  22656  ptcmplem1  22660  ptcmplem2  22661  cnextfres1  22676  tmdgsum  22703  distgp  22707  tgpconncomp  22721  tsmsfbas  22736  tsmsres  22752  tsmsf1o  22753  trust  22838  restutopopn  22847  utop2nei  22859  ussid  22869  isusp  22870  resspwsds  22982  imasdsf1olem  22983  xpsdsval  22991  xblss2ps  23011  xblss2  23012  setsmstopn  23088  tmsval  23091  imasf1obl  23098  prdsxmslem2  23139  tmsxpsval2  23149  nghmfval  23331  isnghm  23332  nmoix  23338  icopnfcld  23376  iocmnfcld  23377  blcvx  23406  icccmplem1  23430  icccmp  23433  xrge0gsumle  23441  xrge0tsms  23442  fsumcn  23478  cnmpopc  23532  xrhmeo  23550  cnheiborlem  23558  bndth  23562  lebnumlem3  23567  htpycom  23580  htpycc  23584  reparphti  23601  pco0  23618  pco1  23619  pcoval2  23620  pcocn  23621  copco  23622  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevcl  23629  pcorevlem  23630  pi1xfrf  23657  pi1xfrcnv  23661  pi1cof  23663  cphassir  23819  tcphds  23834  cphipval  23846  caufval  23878  bcth3  23934  csbren  24002  rrxdstprj1  24012  minveclem2  24029  minveclem3b  24031  minveclem5  24036  ovollb2lem  24089  ovolctb  24091  ovolunlem1a  24097  ovoliunlem1  24103  ovoliunlem2  24104  ovoliunnul  24108  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  shftmbl  24139  iundisj2  24150  voliunlem1  24151  voliunlem3  24153  volsup  24157  ioombl1  24163  icombl  24165  ioombl  24166  iccvolcl  24168  ovolioo  24169  ioovolcl  24171  uniiccdif  24179  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombl  24190  dyaddisjlem  24196  vitalilem5  24213  mbfima  24231  ismbf2d  24241  mbfres2  24246  mbfss  24247  mbfimaopnlem  24256  cncombf  24259  mbflimsup  24267  itg1val2  24285  itg1addlem4  24300  mbfmullem  24326  itg2mulc  24348  itg2splitlem  24349  itg2cnlem1  24362  itgz  24381  itgvallem  24385  itgvallem3  24386  ibl0  24387  itgcnlem  24390  iblrelem  24391  iblposlem  24392  itgrevallem1  24395  iblss2  24406  itgitg2  24407  itgss  24412  itgioo  24416  ibladdlem  24420  itgaddlem1  24423  itgfsum  24427  itgsplitioo  24438  itgcn  24443  ditgneg  24455  limcnlp  24476  limcflf  24479  limccnp2  24490  dvbsss  24500  perfdvf  24501  dvcnp2  24517  dvnp1  24522  dvcmul  24541  dvcmulf  24542  dvcobr  24543  dvexp  24550  dvexp2  24551  dvcnvlem  24573  dveflem  24576  dvef  24577  dvsincos  24578  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dvlip2  24592  dveq0  24597  dv11cn  24598  dvivthlem1  24605  dvivth  24607  lhop2  24612  lhop  24613  dvfsumabs  24620  ftc2  24641  itgsubstlem  24645  mdeg0  24664  deg1val  24690  ply1nzb  24716  q1peqb  24748  ply1remlem  24756  fta1g  24761  fta1blem  24762  ig1pval2  24767  plyeq0lem  24800  plypf1  24802  plymullem1  24804  plyadd  24807  plymul  24808  coeeulem  24814  coeeu  24815  coeid  24828  dgrle  24833  0dgrb  24836  coefv0  24838  coeaddlem  24839  coemullem  24840  dgreq0  24855  dgrmulc  24861  dgrcolem1  24863  dgrcolem2  24864  dgrco  24865  plycj  24867  plymul0or  24870  plydivlem4  24885  plydiveu  24887  plyrem  24894  facth  24895  fta1lem  24896  fta1  24897  quotcan  24898  vieta1lem1  24899  vieta1lem2  24900  vieta1  24901  plyexmo  24902  elqaalem2  24909  elqaa  24911  iaa  24914  aacjcl  24916  aannenlem2  24918  aalioulem3  24923  aalioulem4  24924  aaliou3lem2  24932  tayl0  24950  dvtaylp  24958  taylthlem1  24961  taylthlem2  24962  ulmdvlem1  24988  pserulm  25010  pserdvlem2  25016  pserdv  25017  abelthlem2  25020  abelthlem6  25024  abelthlem9  25028  pilem2  25040  sin2kpi  25069  cos2kpi  25070  coseq00topi  25088  coseq0negpitopi  25089  tanabsge  25092  sincosq1eq  25098  pige3ALT  25105  sinkpi  25107  coskpi  25108  sineq0  25109  tanregt0  25123  efif1olem4  25129  efsubm  25135  logeq0im1  25161  lognegb  25173  logfac  25184  logcj  25189  argregt0  25193  argimgt0  25195  argimlt0  25196  logimul  25197  logneg2  25198  tanarg  25202  logcnlem4  25228  logcn  25230  advlog  25237  advlogexp  25238  logtayl  25243  logccv  25246  0cxp  25249  1cxp  25255  mulcxplem  25267  cxpmul2  25272  cxpsqrt  25286  cxpsqrtth  25312  dvcxp1  25321  dvsqrt  25323  dvcncxp1  25324  dvcnsqrt  25325  cxpcn3lem  25328  cxpcn3  25329  cxpaddlelem  25332  abscxpbnd  25334  root1id  25335  root1eq1  25336  root1cj  25337  cxpeq  25338  loglesqrt  25339  ang180lem1  25387  ang180lem3  25389  ang180lem4  25390  pythag  25395  isosctrlem1  25396  isosctrlem2  25397  1cubr  25420  dcubic2  25422  dcubic  25424  mcubic  25425  cubic2  25426  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  asinlem  25446  acosneg  25465  acoscos  25471  reasinsin  25474  acosbnd  25478  atandmcj  25487  atancj  25488  atanlogsublem  25493  cosatan  25499  atanbnd  25504  bndatandm  25507  atans2  25509  dvatan  25513  atantayl2  25516  leibpilem2  25519  leibpi  25520  log2cnv  25522  birthdaylem2  25530  birthdaylem3  25531  efrlim  25547  scvxcvx  25563  jensen  25566  amgmlem  25567  emcllem7  25579  harmonicbnd3  25585  fsumharmonic  25589  lgamgulmlem1  25606  lgamgulmlem2  25607  lgamcvg2  25632  facgam  25643  wilthlem2  25646  ftalem2  25651  ftalem3  25652  ftalem4  25653  ftalem5  25654  basellem2  25659  basellem3  25660  basellem4  25661  basellem5  25662  efnnfsumcl  25680  efvmacl  25697  ppiprm  25728  chtprm  25730  chtdif  25735  efchtdvds  25736  ppidif  25740  chp1  25744  ppiltx  25754  musum  25768  dvdsmulf1o  25771  fsumdvdsmul  25772  chtublem  25787  chtub  25788  logfacbnd3  25799  logexprlim  25801  dchrmulcl  25825  dchrinvcl  25829  dchrfi  25831  dchrabs  25836  dchrinv  25837  dchrptlem2  25841  sum2dchr  25850  bclbnd  25856  bposlem1  25860  bposlem2  25861  bposlem5  25864  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgslem2  25874  lgsfcl2  25879  lgsval2lem  25883  lgs0  25886  lgs2  25890  lgsneg  25897  lgsdilem  25900  lgsdir2lem4  25904  lgsdir2lem5  25905  lgsdilem2  25909  lgsne0  25911  lgssq  25913  lgssq2  25914  gausslemma2dlem3  25944  gausslemma2dlem4  25945  lgseisenlem1  25951  lgsquadlem2  25957  lgsquad2lem2  25961  lgsquad3  25963  m1lgs  25964  2lgslem1a2  25966  2lgsoddprmlem3  25990  2sqlem9  26003  2sqlem10  26004  2sqlem11  26005  2sqb  26008  2sq2  26009  2sqnn  26015  2sqreultlem  26023  2sqreunnltlem  26026  chebbnd1lem1  26045  chebbnd1lem3  26047  chto1lb  26054  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasum2lem  26072  dchrisum0fval  26081  dchrisum0ff  26083  dchrisum0flblem1  26084  rpvmasum2  26088  rpvmasum  26102  mulogsum  26108  logdivsum  26109  mulog2sumlem2  26111  log2sumbnd  26120  selberg2lem  26126  logdivbnd  26132  pntrsumo1  26141  pntrsumbnd2  26143  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntibndlem3  26168  pntlemg  26174  pntleml  26187  ostth2lem2  26210  ostth3  26214  tgcgr4  26317  perpln1  26496  colperpexlem1  26516  hpgbr  26546  ttgval  26661  brbtwn2  26691  ax5seglem4  26718  axpaschlem  26726  axlowdimlem6  26733  axlowdimlem16  26743  axlowdim  26747  axeuclid  26749  axcontlem2  26751  axcontlem4  26753  axcontlem8  26757  elntg2  26771  isuhgr  26845  isushgr  26846  uhgr0vb  26857  uhgrun  26859  incistruhgr  26864  isupgr  26869  isumgr  26880  umgrnloop0  26894  upgrun  26903  umgrun  26905  umgrislfupgrlem  26907  isuspgr  26937  isusgr  26938  usgrnloop0ALT  26987  usgrf1oedg  26989  usgredg3  26998  lfuhgr1v0e  27036  usgrexmplef  27041  usgrexmplvtx  27043  egrsubgr  27059  0uhgrsubgr  27061  uhgrspansubgrlem  27072  nbgr0vtx  27138  nbgr1vtx  27140  nb3grpr  27164  nb3grpr2  27165  uvtx0  27176  uvtx01vtx  27179  cplgr1v  27212  cusgrsizeindb1  27232  vtxdg0v  27255  vtxdg0e  27256  vtxdun  27263  vtxdlfgrval  27267  1loopgrvd2  27285  umgr2v2evd2  27309  vtxdginducedm1  27325  finsumvtxdg2size  27332  wlkl1loop  27419  wlkson  27438  2wlklem  27449  upgr2wlk  27450  wlkreslem  27451  wlkp1  27463  uhgrwkspthlem2  27535  usgr2wlkneq  27537  usgr2wlkspthlem2  27539  usgr2trlncl  27541  usgr2pth  27545  pthdlem1  27547  pthdlem2  27549  uspgrn2crct  27586  crctcshwlkn0lem6  27593  wwlksn  27615  wspthsn  27626  iswwlksnon  27631  iswspthsnon  27634  wwlksn0s  27639  wwlksnfi  27684  wwlksnfiOLD  27685  wspn0  27703  2wlkdlem5  27708  2wlkdlem10  27714  umgrwwlks2on  27736  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlkl1  27747  rusgr0edg  27752  clwlkclwwlklem2a4  27775  clwlkclwwlkfo  27787  clwwlkneq0  27807  clwwlkn1  27819  clwwlkn2  27822  clwwlkwwlksb  27833  wwlksext2clwwlk  27836  umgr2cwwk2dif  27843  clwwlk0on0  27871  clwwlknon0  27872  clwwlknonel  27874  clwwlknon1  27876  clwwlknon1le1  27880  clwwlknonex2lem1  27886  1wlkdlem4  27919  3wlkdlem5  27942  3wlkdlem10  27948  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth0  27993  trlsegvdeglem4  28002  eupthvdres  28014  eupth2lemb  28016  eucrct2eupth  28024  frcond3  28048  frgr1v  28050  frgr3v  28054  1vwmgr  28055  3vfriswmgr  28057  1to3vfriswmgr  28059  frgrwopregbsn  28096  fusgr2wsp2nb  28113  2clwwlk2clwwlklem  28125  2clwwlk2  28127  numclwlk1lem1  28148  numclwwlkovh  28152  numclwlk2lem2f  28156  numclwwlk3lem2  28163  frgrregord013  28174  ex-pw  28208  ex-pr  28209  ex-dm  28218  ex-rn  28219  ex-res  28220  ex-ima  28221  ex-fv  28222  ex-ceil  28227  ipval2  28484  ipidsq  28487  diporthcom  28493  dip0r  28494  dip0l  28495  nmoo0  28568  nmlno0lem  28570  nmlnoubi  28573  ipasslem2  28609  pythi  28627  siilem1  28628  siii  28630  minvecolem2  28652  hvmul0  28801  hvsubid  28803  hvaddsubval  28810  hvsubeq0i  28840  hvsub0  28853  hi02  28874  orthcom  28885  bcseqi  28897  normgt0  28904  normpythi  28919  hsn0elch  29025  ocsh  29060  shjcom  29135  omlsilem  29179  pjoc1i  29208  ssjo  29224  shs00i  29227  chj00i  29264  h1de2bi  29331  h1datomi  29358  fh1  29395  fh2  29396  cm2j  29397  nonbooli  29428  pjssge0ii  29459  hosubeq0i  29603  eigrei  29611  eigorthi  29614  bra0  29727  kbpj  29733  0cnop  29756  0cnfn  29757  0lnfn  29762  nmop0  29763  nmfn0  29764  nmop0h  29768  nmlnop0iALT  29772  lnopco0i  29781  lnopeq0i  29784  nmcoplbi  29805  nmophmi  29808  nmbdfnlbi  29826  nmcfnlbi  29829  nlelshi  29837  adjeq0  29868  nmopcoi  29872  unierri  29881  nmopleid  29916  opsqrlem1  29917  pjsdi2i  29934  pjclem1  29972  hstnmoc  30000  hst1h  30004  strlem3a  30029  strlem4  30031  golem1  30048  stcltrlem1  30053  mdsl1i  30098  mdslmd3i  30109  csmdsymi  30111  atoml2i  30160  atordi  30161  atabsi  30178  sumdmdlem2  30196  cdj3lem1  30211  unidifsnel  30295  unidifsnne  30296  difuncomp  30305  iuninc  30312  disjdifprg  30325  disji2f  30327  disjif2  30331  disjabrex  30332  disjabrexf  30333  disjpreima  30334  iundisj2f  30340  difres  30350  imadifxp  30351  funresdm1  30355  fnresin  30371  f1o3d  30372  eldmne0  30373  dfimafnf  30381  ofrn2  30387  xppreima  30394  abfmpeld  30399  abfmpel  30400  aciunf1lem  30407  aciunf1  30408  ofpreima  30410  ofpreima2  30411  fnpreimac  30416  coprprop  30435  padct  30455  ffsrn  30465  resf1o  30466  fpwrelmapffslem  30468  1neg1t1neg1  30473  fzdif2  30514  fzodif2  30515  fzodif1  30516  iundisj2fi  30520  f1ocnt  30525  hashxpe  30529  nn0min  30536  s3f1  30623  swrdrndisj  30631  cshw1s2  30634  xrsmulgzz  30665  xrge0npcan  30681  gsummpt2co  30686  xrge0tsmsd  30692  gsumle  30725  symgcom  30727  odpmco  30730  pmtrcnel2  30734  fzto1st  30745  tocycf  30759  tocyc01  30760  cycpm2tr  30761  cycpmco2f1  30766  cycpmconjv  30784  tocyccntz  30786  cyc3evpm  30792  cycpmconjslem2  30797  cyc3conja  30799  archirngz  30818  qsidomlem1  30965  lvecdim0  31005  rgmoddim  31008  rrxdim  31012  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  fldexttr  31048  smatlem  31062  lmat22lem  31082  madjusmdetlem4  31095  locfinref  31105  metider  31134  pstmfval  31136  hauseqcn  31138  ordtcnvNEW  31163  ordtconnlem1  31167  xrge0iifiso  31178  xrge0iifhom  31180  indval2  31273  esumval  31305  esumnul  31307  esum0  31308  esumsnf  31323  esumrnmpt2  31327  esumpfinval  31334  esumpfinvalf  31335  esum2dlem  31351  0elsiga  31373  prsiga  31390  unelldsys  31417  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  fiunelros  31433  measxun2  31469  measun  31470  measvunilem0  31472  measvuni  31473  measinb  31480  cntmeas  31485  cntnevol  31487  ddemeas  31495  aean  31503  mbfmcst  31517  mbfmcnt  31526  dya2iocuni  31541  omssubadd  31558  carsgval  31561  difelcarsg  31568  inelcarsg  31569  carsgclctunlem1  31575  carsggect  31576  carsgclctunlem2  31577  carsgclctunlem3  31578  carsgclctun  31579  omsmeas  31581  issibf  31591  sibf0  31592  sibfof  31598  sitg0  31604  sitmcl  31609  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgf  31637  fibp1  31659  probun  31677  0rrv  31709  dstrvprob  31729  coinflippv  31741  ballotlemfp1  31749  ballotlemfval0  31753  ballotlemsv  31767  sgncl  31796  sgnneg  31798  sgnmul  31800  plymulx0  31817  signsw0glem  31823  signstf0  31838  signstfvn  31839  signsvtn0  31840  signstfvp  31841  signstfvneq0  31842  signstfveq0a  31846  signstfveq0  31847  signsvf1  31851  signsvfn  31852  signshf  31858  itgexpif  31877  fsum2dsub  31878  reprdifc  31898  chtvalz  31900  breprexplemc  31903  breprexp  31904  circlemethhgt  31914  hgt750lemd  31919  tgoldbachgtda  31932  lpadlem3  31949  lpadright  31955  bnj571  32178  bnj1416  32311  spthcycl  32376  derangsn  32417  subfacp1lem1  32426  subfacp1lem2a  32427  subfacp1lem5  32431  subfacp1lem6  32432  subfacval2  32434  subfacval3  32436  erdsze2lem2  32451  indispconn  32481  cvxpconn  32489  cvxsconn  32490  cvmscld  32520  cvmliftlem10  32541  cvmlift2lem13  32562  cvmliftphtlem  32564  satfv0  32605  satfv1  32610  satfdm  32616  satfrnmapom  32617  fmlasuc0  32631  satffunlem1lem2  32650  satfv0fvfmla0  32660  sate0  32662  ex-sategoelel  32668  elnanelprv  32676  prv1n  32678  mdvval  32751  mrsubfval  32755  mrsub0  32763  elmrsubrn  32767  mrsubvrs  32769  elmsubrn  32775  mclsrcl  32808  mthmval  32822  sinccvglem  32915  nepss  32948  climlec3  32965  bcprod  32970  bccolsum  32971  faclimlem1  32975  faclim  32978  eldm3  32997  opelco3  33018  elima4  33019  trpred0  33075  frrlem12  33134  noextendseq  33174  nosupdm  33204  nosupbday  33205  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1  33214  nosupbnd2  33216  noetalem4  33220  madeval2  33290  unisnif  33386  funpartlem  33403  fvline  33605  lineunray  33608  fwddifn0  33625  fwddifnp1  33626  rankeq1o  33632  topbnd  33672  fnessref  33705  neibastop2lem  33708  ordcmp  33795  bj-projval  34311  bj-funun  34537  bj-fununsn2  34539  mptsnunlem  34622  dissneqlem  34624  finxp00  34686  pibt2  34701  finixpnum  34892  sin2h  34897  tan2h  34899  lindsadd  34900  lindsenlbs  34902  matunitlindflem1  34903  matunitlindf  34905  ptrest  34906  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  broucube  34941  heicant  34942  mblfinlem2  34945  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  mbfposadd  34954  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  itg2addnc  34961  ibladdnclem  34963  itgaddnclem1  34965  itgaddnclem2  34966  iblmulc2nc  34972  ftc1anclem1  34982  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  dvasin  34993  areacirclem1  34997  areacirclem4  35000  areacirc  35002  sdclem2  35032  fdc  35035  mettrifi  35047  sstotbnd2  35067  isbnd3  35077  bndss  35079  totbndbnd  35082  ismtyval  35093  heiborlem7  35110  heiborlem8  35111  rrncmslem  35125  exidreslem  35170  grposnOLD  35175  divrngcl  35250  isdrngo2  35251  ispridlc  35363  br1cosscnvxrn  35729  n0el3  35900  l1cvat  36206  lshpkrlem1  36261  ldualsmul  36286  cmtvalN  36362  cvrval  36420  glbconxN  36529  pmapglb2xN  36923  padd01  36962  padd02  36963  pmod2iN  37000  pmodl42N  37002  polval2N  37057  pol0N  37060  pclfinclN  37101  osumcllem3N  37109  ltrncnvnid  37278  cdleme13  37423  cdleme31sn1  37532  cdleme31snd  37537  cdleme31sn2  37540  cdleme40v  37620  cdlemeg46vrg  37678  tendoplcbv  37926  tendoicbv  37944  erng1r  38146  dvalveclem  38176  dva0g  38178  dia2dimlem2  38216  dvhvaddass  38248  dvhlveclem  38259  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetALTN  38478  lcfl7N  38652  lcdsmul  38753  mapdhval0  38876  hdmap1val0  38950  hdmap11lem2  38993  2xp3dxp2ge1d  39117  frlmsnic  39169  nn0rppwr  39202  remulinvcom  39268  3cubeslem1  39301  rntrclfvOAI  39308  mapfzcons2  39336  mzpmfp  39364  fzsplit1nn0  39371  diophrw  39376  eldioph2lem1  39377  eldioph2lem2  39378  eldioph2  39379  eldioph3  39383  eq0rabdioph  39393  rexrabdioph  39411  elnn0rabdioph  39420  diophren  39430  pellexlem5  39450  pellex  39452  pell1qr1  39488  pell1qrgaplem  39490  jm2.18  39605  jm2.27dlem1  39626  fnwe2lem1  39670  kelac2lem  39684  pwssplit4  39709  pwfi2f1o  39716  dgrsub2  39755  mpaaeu  39770  mon1pid  39825  fgraphopab  39830  arearect  39842  areaquad  39843  rp-isfinite6  39904  pwelg  39939  relintab  39963  elcnvlem  39981  conrel1d  40028  restrreld  40032  trrelsuperrel2dg  40036  dfrcl2  40039  iunrelexp0  40067  relexpiidm  40069  trclrelexplem  40076  dftrcl3  40085  trclfvcom  40088  cnvtrclfv  40089  trclimalb2  40091  dmtrclfvRP  40095  rntrclfv  40097  dfrtrcl3  40098  cotrclrcl  40107  frege109d  40122  frege124d  40126  frege131d  40129  rfovcnvf1od  40370  fsovrfovd  40375  dssmapnvod  40386  ntrk0kbimka  40409  clsk3nimkb  40410  clsk1indlem3  40413  clsk1indlem4  40414  clsk1indlem1  40415  ntrclscls00  40436  ntrneiel2  40456  clsneibex  40472  neicvgbex  40482  neicvgnvo  40485  mnuprdlem1  40628  mnuprdlem2  40629  radcnvrat  40666  nzss  40669  lhe4.4ex1a  40681  dvsef  40684  expgrowth  40687  bccn0  40695  binomcxplemnn0  40701  binomcxplemradcnv  40704  binomcxplemdvbinom  40705  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  compne  40793  sineq0ALT  41291  refsum2cnlem1  41314  dffo3f  41458  wessf1ornlem  41465  disjrnmpt2  41469  founiiun0  41471  feqresmptf  41519  fzisoeu  41587  infxrpnf  41741  iccdifprioo  41812  qinioo  41831  fmuldfeqlem1  41883  mulc1cncfg  41890  constlimc  41925  sumnnodd  41931  limsup10ex  42074  liminf10ex  42075  liminflbuz2  42116  liminfpnfuz  42117  fperdvper  42223  dvresioo  42226  dvcosax  42231  dvnprodlem3  42253  itgsin0pilem1  42255  itgsinexplem1  42259  stoweidlem9  42314  stoweidlem13  42318  stoweidlem17  42322  stoweidlem34  42339  stoweidlem35  42340  stoweidlem36  42341  stoweidlem37  42342  stoweidlem39  42344  wallispilem2  42371  wallispilem4  42373  wallispi2lem2  42377  dirkerval2  42399  dirkerper  42401  dirkertrigeqlem1  42403  dirkertrigeqlem3  42405  dirkeritg  42407  dirkercncflem2  42409  fourierdlem30  42442  fourierdlem42  42454  fourierdlem60  42471  fourierdlem61  42472  fourierdlem62  42473  fourierdlem72  42483  fourierdlem75  42486  fourierdlem80  42491  fourierdlem81  42492  fourierdlem83  42494  fourierdlem94  42505  fourierdlem104  42515  fourierdlem105  42516  fourierdlem108  42519  fourierdlem111  42522  fourierdlem113  42524  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  fouriercn  42537  elaa2  42539  etransclem14  42553  etransclem24  42563  etransclem25  42564  etransclem35  42574  etransclem44  42583  etransclem46  42585  prsal  42623  sge0iunmptlemfi  42715  nnfoctbdjlem  42757  caragenunicl  42826  ovnsubadd  42874  funcoressn  43297  fnrnafv  43381  fvifeq  43499  fzopredsuc  43543  1fzopredsuc  43544  2ffzoeq  43548  uniimaelsetpreimafv  43576  iccpartiltu  43602  iccpartigtl  43603  iccpartlt  43604  iccelpart  43613  sprvalpwn0  43665  fmtnorec2lem  43724  fmtnorec3  43730  fmtnofac1  43752  fmtno4prmfac  43754  mod42tp1mod8  43787  lighneallem2  43791  lighneallem3  43792  sbgoldbaltlem1  43964  nnsum3primes4  43973  nnsum3primesprm  43975  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  isomushgr  44011  ushrisomgr  44026  uspgrsprfo  44043  fnxpdmdm  44055  1odd  44098  0ringdif  44161  c0snmhm  44206  uzlidlring  44220  rnghmsubcsetclem1  44266  rnghmsubcsetc  44268  rngcifuestrc  44288  funcrngcsetc  44289  funcrngcsetcALT  44290  rhmsubcsetclem1  44312  rhmsubcsetc  44314  rhmsubcrngclem1  44318  rhmsubcrngc  44320  rngcresringcat  44321  funcringcsetc  44326  rngcrescrhm  44376  rhmsubc  44381  rngcrescrhmALTV  44394  rhmsubcALTVlem3  44397  mndpsuppss  44439  ply1mulgsum  44464  lincval0  44490  lco0  44502  linds0  44540  zlmodzxzequap  44574  ldepsnlinc  44583  blen1  44664  blen1b  44668  0dig1  44689  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700  nn0sumshdiglem1  44701  nn0sumshdiglem2  44702  prelrrx2b  44721  line2ylem  44758  line2x  44761  2itscp  44788  onetansqsecsq  44880  cotsqcscsq  44881  aacllem  44922