Theorem eqidd 2764

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2763	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755

This theorem is referenced by:  nfabd2  2948  neleq1  3068  neleq2  3069  elabd3  3631  nelrdva  3669  sbcbidv  3800  csbie2df  4398  reusngf  4634  rexreusng  4639  reuprg0  4662  iunxdif3  5053  mpteq1  5190  mpteq1i  5192  mpteq2da  5193  mpteq2dva  5194  nfcvb  5334  dfid2  5545  feq23d  6687  f10d  6842  fvmptdv2  6995  elrnrexdm  7071  f1ossf1o  7111  fmptco  7112  cofmpt  7115  fprg  7139  ftpg  7140  fmptsng  7153  fmptsnd  7154  f1dom3fv3dif  7253  f1dom3el3dif  7254  fliftfun  7297  fliftval  7301  nfriotad  7365  cbvmpo  7491  fconstmpo  7514  eqfnov2  7527  ovmpod  7549  ovmpodv2  7555  fvmpopr2d  7559  elovmporab  7643  elovmporab1w  7644  elovmporab1  7645  ovmpt3rab1  7655  elovmpt3rab  7658  ofval  7672  ofrval  7673  offn  7674  fnfvof  7678  off  7679  ofres  7680  coof  7685  ofco  7686  caofref  7692  caofid0l  7694  caofid0r  7695  caofid1  7696  caofid2  7697  caofrss  7700  caoftrn  7702  tfisi  7840  fsplitfpar  8098  fczsupp0  8174  suppssof1  8180  suppofss1d  8185  suppofss2d  8186  fvmpocurryd  8252  fpr3g  8267  iserd  8706  fsetfocdm  8843  ixpsnf1o  8921  mapxpen  9116  dffi3  9378  cantnf0  9631  cantnfp1  9637  cantnflem1  9645  ttrcltr  9672  axcclem  10415  ttukeylem3  10469  fpwwe2lem8  10597  ofsubeq0  12193  ofnegsub  12194  ofsubge0  12195  fzo0to3tp  13759  fzo1to4tp  13761  modsubmod  13943  seqid  14061  seqid2  14062  seqz  14064  seqof  14073  elovmptnn0wrd  14573  ccatdmss  14596  ccatws1ls  14648  pfxsuffeqwrdeq  14712  wrdind  14736  wrd2ind  14737  ccats1pfxeqbi  14756  repswsymb  14788  repswsymball  14793  repswsymballbi  14794  s3eq2  14884  swrds2m  14955  wrdl2exs2  14960  swrd2lsw  14966  wwlktovfo  14972  s3sndisj  14981  s3iunsndisj  14982  relexp0g  15036  relexpsucnnr  15039  relexp1g  15040  rtrclreclem1  15071  rtrclreclem4  15075  dfrtrcl2  15076  sgnneg  15114  rlim2  15524  climcl  15527  rlimcl  15531  clim2  15532  rlimclim1  15573  rlimclim  15574  climrlim2  15575  climuni  15580  rlimres  15586  climeq  15595  2clim  15600  climshftlem  15602  climabs0  15613  climcn1  15620  climcn2  15621  o1of2  15641  o1rlimmul  15647  o1add2  15652  o1mul2  15653  o1sub2  15654  o1dif  15658  climsqz  15669  climsqz2  15670  rlimdiv  15674  isercoll  15696  climsup  15698  climcau  15699  caurcvgr  15702  caucvgb  15708  serf0  15709  iseralt  15713  sumz  15750  fsumss  15753  fsumsplitsn  15772  fsumsplit1  15773  fsumsplitsnun  15783  isumclim3  15787  isummulc2  15790  fsum2dlem  15798  fsumconst  15818  fsumabs  15830  fsumparts  15835  fsumrlim  15840  fsumo1  15841  seqabs  15843  cvgcmpce  15847  fsumiun  15850  ackbijnn  15859  isumshft  15870  isumltss  15879  climcndslem1  15880  climcndslem2  15881  climcnds  15882  mertenslem1  15915  mertenslem2  15916  prod1  15975  fprodss  15979  fprodconst  16009  fprod2dlem  16011  fprodsplitsn  16020  iprodclim3  16031  eftlcl  16140  reeftlcl  16141  eftlub  16142  efsep  16143  effsumlt  16144  eirrlem  16237  rpnnen2lem6  16252  rpnnen2lem7  16253  rpnnen2lem8  16254  rpnnen2lem9  16255  rpnnen2lem12  16258  2tp1odd  16387  sadasslem  16505  smupvallem  16518  smumul  16528  alginv  16610  algfx  16615  cncongr1  16702  qnumdencoprm  16781  qeqnumdivden  16782  vdwlem1  17018  vdwlem12  17029  vdwlem13  17030  prmodvdslcmf  17084  prmgap  17096  prmgaplcm  17097  prmgapprmo  17099  setsexstruct2  17212  setsstruct  17213  prdssca  17486  prdsbas  17487  prdsplusg  17488  prdsmulr  17489  prdsvsca  17490  prdsip  17491  prdsle  17492  prdsds  17494  prdstset  17496  prdshom  17497  prdsco  17498  prdsvscafval  17510  prdsdsval2  17514  prdsdsval3  17515  pwsle  17523  pwsleval  17524  pwsvscaval  17526  imasbas  17543  imasds  17544  imasplusg  17548  imasmulr  17549  imassca  17550  imasvsca  17551  imasip  17552  imastset  17553  imasle  17554  imasvscafn  17568  imasvscaval  17569  qusin  17575  xpsvsca  17608  iscat  17705  iscatd  17706  iscatd2  17714  0catg  17721  homfeq  17727  homfeqd  17728  comfffval2  17734  comffval2  17735  comfeq  17739  comfeqd  17740  oppccatid  17752  2oppccomf  17758  moni  17770  rcaninv  17828  ssc2  17856  ssctr  17859  ssceq  17860  subcssc  17874  subccat  17882  subsubc  17887  funcres  17930  funcres2  17932  idfusubc  17934  funcres2c  17937  idffth  17969  cofull  17970  cofth  17971  ressffth  17974  isnat  17984  fuccofval  17996  fuccatid  18006  fucpropd  18014  elhomai  18067  coafval  18098  setcval  18111  setcbas  18112  setchomfval  18113  setccofval  18116  setcco  18117  setccatid  18118  setcepi  18122  funcsetcres2  18127  catcval  18134  catcbas  18135  catchomfval  18136  catccofval  18138  catcco  18139  catccatid  18140  catcfuccl  18152  estrcval  18157  estrcbas  18158  estrchomfval  18159  estrccofval  18162  estrcco  18163  estrccatid  18165  estrreslem2  18171  fullestrcsetc  18184  fullsetcestrc  18199  xpcbas  18211  xpchomfval  18212  xpccofval  18215  xpccatid  18221  prfval  18232  catcxpccl  18240  xpcpropd  18241  evlfval  18250  curfval  18256  curf1  18258  curf12  18260  curf2  18262  curf2val  18263  hofval  18285  hof2fval  18288  hofcllem  18291  oppchofcl  18293  oppcyon  18302  oyoncl  18303  yonedalem4a  18308  yonedalem4b  18309  yonedainv  18314  oduposb  18360  joinval  18408  meetval  18422  isdlat  18555  ipopos  18569  pfxchn  18643  chnind  18654  chnso  18657  chnccats1  18658  chnccat  18659  chnrev  18660  gsumpropd  18713  gsumpropd2lem  18714  gsumval1  18718  gsumval2a  18720  issgrp  18755  issgrpd  18765  prdssgrpd  18768  ismndd  18791  mndprop  18795  prdsmndd  18805  imasmnd2  18809  insubm  18853  mhmima  18860  frmdbas  18887  frmdmnd  18894  efmnd  18905  smndex1gid  18939  smndex1gidOLD  18940  smndex1n0mnd  18950  smndex2dlinvh  18955  sgrpnmndex  18970  resgrpplusfrn  18993  grpprop  18995  grpsubfval  19026  grpsubfvalALT  19027  grpsubpropd  19088  prdsgrpd  19093  imasgrp2  19098  imasgrp  19099  imasgrpf1  19100  mulgfval  19112  mulgfvalALT  19113  mulgnngsum  19122  mulgnn0gsum  19123  mulgpropd  19159  subgsub  19181  eqgfval  19218  qusgrp  19228  ghmqusnsglem1  19321  ghmqusnsglem2  19322  ghmqusnsg  19323  ghmquskerlem1  19324  ghmquskerlem2  19326  ghmquskerlem3  19327  ghmqusker  19328  oppgmnd  19395  oppgmndb  19396  oppggrp  19398  oppggrpb  19399  symgval  19412  symg1bas  19432  symg2bas  19434  symgvalstruct  19438  symggrp  19441  gsmsymgrfixlem1  19468  gsmsymgreqlem2  19472  symgfixels  19475  symgsssg  19508  symgfisg  19509  psgnunilem4  19538  psgnvalii  19550  oppglsm  19683  lsmelvalmi  19693  efgi0  19761  efgi1  19762  efgtf  19763  efgval2  19765  efginvrel2  19768  frgp0  19801  frgpup3lem  19818  ablprop  19834  subcmn  19878  gex2abl  19892  prdscmnd  19902  qusabl  19906  abl1  19907  cygabl  19932  gsumzf1o  19953  gsumzaddlem  19962  gsumzsplit  19968  gsumconst  19975  gsumconstf  19976  gsummptshft  19977  gsummhm2  19980  gsummptmhm  19981  gsumzunsnd  19997  gsumunsnfd  19998  gsumpt  20003  gsummptf1o  20004  gsummptun  20005  gsum2dlem2  20012  gsumcom2  20016  nn0gsumfz  20025  dprdval  20046  dprdssv  20059  dprdfeq0  20065  dprdsubg  20067  dprdspan  20070  dprdz  20073  subgdmdprd  20077  subgdprd  20078  gsumle  20186  isrng  20201  isrngd  20220  prdsrngd  20223  imasrng  20224  issrg  20239  isring  20288  ringabl  20332  ringprop  20341  isringd  20342  prdsringd  20370  prdscrngd  20371  prds1  20372  pwspjmhmmgpd  20377  imasring  20380  opprrng  20395  opprrngb  20396  opprringb  20398  dvrfval  20452  rnghmf1o  20502  c0mgm  20509  c0mhm  20510  c0snmgmhm  20512  c0snmhm  20513  rngisomring1  20518  rhmf1o  20541  pwsco1rhm  20552  pwsco2rhm  20553  zrrnghm  20587  rhmimasubrng  20617  pwsdiagrhm  20658  rngcbas  20672  rngchomfval  20673  dfrngc2  20679  rnghmsscmap2  20680  rnghmsscmap  20681  rngccat  20685  rngcid  20686  funcrngcsetc  20691  funcrngcsetcALT  20692  zrinitorngc  20693  zrtermorngc  20694  ringcbas  20701  ringchomfval  20702  dfringc2  20708  rhmsscmap2  20709  rhmsscmap  20710  ringccat  20714  ringcid  20715  rngcresringcat  20720  funcringcsetc  20725  zrtermoringc  20726  rhmsubc  20740  drngprop  20795  isdrngd  20816  isdrngrd  20817  isdrngdOLD  20818  isdrngrdOLD  20819  abvtrivd  20882  idsrngd  20906  suborng  20926  islmodd  20934  lmodabl  20977  lss1  21006  lsssn0  21016  islss3  21027  lss1d  21031  lssintcl  21032  prdslmodd  21037  idlmhm  21109  invlmhm  21110  lmhmvsca  21113  lbsextlem2  21230  sralmod  21255  sralmod0  21256  rlm0  21263  rlmvneg  21274  rnglidlmsgrp  21317  rnglidlrng  21318  qus2idrng  21344  crngridl  21351  quscrng  21354  rhmqusnsg  21356  rngqiprngimf1lem  21365  rngqiprngimf1  21371  absabv  21477  pzriprnglem10  21543  zrhpropd  21567  fermltlchr  21582  znzrh  21595  znbas  21596  zncrng  21597  znzrhfo  21600  znf1o  21604  frgpcyg  21626  evpmodpmf1o  21649  isphld  21707  phlpropd  21708  phssip  21711  phlssphl  21712  pjfval  21759  dsmmval  21787  dsmmsubg  21796  frlmip  21831  frlmipval  21832  frlmphllem  21833  frlmphl  21834  islindf  21865  islindf4  21891  isassa  21909  isassad  21918  issubassa3  21919  asclfval  21931  ressascl  21949  psrval  21968  psrbaglesupp  21975  psrbagcon  21978  psrbaglefi  21979  psrbagleadd1  21981  psrbagconf1o  21982  gsumbagdiaglem  21984  psrass1lem  21986  psrbas  21987  psrplusg  21990  psrmulr  21995  psrsca  22000  psrvscafval  22001  psrvscaval  22003  psrlmod  22012  psrlidm  22014  psrdi  22017  psrdir  22018  psrcom  22020  psrring  22022  psrassa  22025  mplsubglem  22051  mpllsslem  22052  mplvscaval  22068  mplcoe1  22091  mplcoe3  22092  mplcoe5  22094  opsrcrng  22113  opsrassa  22114  mplmon2  22115  evlslem2  22133  evlslem1  22136  evlsvvval  22147  mplmapghm  22176  evlsmaprhm  22185  selvvvval  22196  selvadd  22197  selvmul  22198  mhpmulcl  22215  psdffval  22223  psdmplcl  22228  psdadd  22229  psdmul  22232  psdmvr  22235  ply1lss  22259  ply1subrg  22260  opsr0  22281  opsr1  22282  subrgply1  22295  psrplusgpropd  22298  psropprmul  22300  opsrring  22307  opsrlmod  22308  ply1mpl0  22319  ply1mpl1  22321  coe1z  22327  coe1mul2  22333  coe1tm  22337  coe1sclmulfv  22347  ply1coe  22362  evls1rhm  22386  evls1sca  22387  evl1rhm  22396  evl1sca  22398  evl1expd  22409  evl1gsumdlem  22420  evl1varpw  22425  evls1maplmhm  22441  mamufval  22453  mamudi  22464  mamudir  22465  mat0  22478  matinvg  22479  matlmod  22490  matinvgcell  22496  matring  22504  matassa  22505  mat0dimcrng  22531  mat1dim0  22534  mat1f1o  22539  dmatmulcl  22561  scmatval  22565  scmatscmiddistr  22569  scmataddcl  22577  scmatsubcl  22578  scmatmulcl  22579  scmatlss  22586  scmatrhmcl  22589  1mavmul  22609  mavmul0  22613  marepvfval  22626  submafval  22640  submaval  22642  mdetleib2  22649  mdet0pr  22653  m1detdiag  22658  mdetrsca  22664  mdetrsca2  22665  mdetrlin2  22668  mdetralt  22669  mdetralt2  22670  mdetunilem2  22674  mdetunilem5  22677  mdetunilem9  22681  mdetuni0  22682  m2detleib  22692  madufval  22698  symgmatr01lem  22714  symgmatr01  22715  gsummatr01lem3  22718  gsummatr01lem4  22719  gsummatr01  22720  smadiadetlem3  22729  smadiadetglem2  22733  smadiadetr  22736  mat2pmatghm  22791  cpm2mfval  22810  m2cpminvid  22814  m2cpminvid2lem  22815  m2cpminvid2  22816  decpmatval  22826  decpmataa0  22829  decpmatmul  22833  pmatcollpw1  22837  pmatcollpw2lem  22838  monmatcollpw  22840  pmatcollpwlem  22841  pmatcollpw  22842  pmatcollpwscmatlem2  22851  pm2mpval  22856  pm2mpcl  22858  pm2mpf1  22860  mptcoe1matfsupp  22863  mp2pm2mplem3  22869  mp2pm2mplem4  22870  pm2mpghm  22877  pm2mpmhmlem2  22880  chpmat1dlem  22896  chp0mat  22907  fvmptnn04ifa  22911  fvmptnn04ifb  22912  fvmptnn04ifc  22913  fvmptnn04ifd  22914  cpmadugsumlemB  22935  chcoeffeqlem  22946  epttop  23070  ordtbas2  23252  ordtopn1  23255  ordtopn2  23256  lmss  23359  2ndci  23509  2ndcsep  23520  dis2ndc  23521  1stcelcls  23522  dissnlocfin  23590  ptbasid  23636  xkoopn  23650  prdstopn  23689  ptrescn  23700  txlm  23709  lmcn2  23710  tx1stc  23711  xkopt  23716  cnmpt2c  23731  cnmptk1  23742  cnmpt1k  23743  cnmptkk  23744  qtopeu  23777  txswaphmeolem  23865  xpstopnlem1  23870  ptcmpfi  23874  xkohmeo  23876  rnelfmlem  24013  rnelfm  24014  hauspwpwf1  24048  lmflf  24066  flfcnp2  24068  alexsubb  24107  tmdgsum  24156  tgpconncomp  24174  qustgphaus  24184  tsmsfbas  24189  tsmspropd  24193  tsmssplit  24213  tsmsxplem1  24214  tsmsxplem2  24215  ustuqtop4  24305  imasdsf1olem  24434  blfvalps  24444  stdbdxmet  24576  met2ndci  24583  prdsxmslem2  24590  metustexhalf  24617  cfilucfil  24620  restmetu  24631  nmfval  24649  nmpropd  24655  nmpropd2  24656  subgnm  24694  tng0  24704  tngnm  24712  tnggrpr  24716  tngngp3  24717  tngnrg  24735  sranlm  24745  qdensere  24830  mpomulcn  24930  fsumcn  24933  cncfcompt2  24971  cncfmpt1f  24977  negfcncf  24986  oprpiece1res2  25015  htpyid  25040  phtpyid  25052  pcofval  25073  pcopt2  25086  om1bas  25094  om1plusg  25097  om1tset  25098  pi1bas  25101  pi1bas2  25104  pi1eluni  25105  pi1bas3  25106  pi1cpbl  25107  pi1addf  25110  pi1addval  25111  pi1grplem  25112  pi1xfr  25118  pi1xfrcnvlem  25119  pi1coghm  25124  cphassr  25275  tcphphl  25290  ipcau2  25297  cphipval  25306  lmnn  25326  iscau  25339  cmetcaulem  25351  iscmet3lem1  25354  causs  25361  lmclim  25366  srabn  25423  rrxprds  25452  rrxip  25453  rrxcph  25455  rrxds  25456  rrxmvallem  25467  rrxmval  25468  rrxdsfival  25476  ehl2eudisval  25486  divcncf  25510  ovollb2lem  25551  ovolfiniun  25564  ovolicc2lem4  25583  shftmbl  25601  volfiniun  25610  ioombl1lem4  25624  uniioombllem2  25646  uniioombllem6  25651  vitalilem4  25674  mbfmulc2lem  25710  mbfmulc2re  25711  mbfneg  25713  mbfaddlem  25723  mbfadd  25724  mbfsub  25725  mbfmulc2  25726  0plef  25735  0pledm  25736  itg1ge0  25749  i1faddlem  25756  i1fmullem  25757  i1fmulclem  25765  itg1mulc  25767  itg1lea  25775  itg1le  25776  mbfi1flimlem  25785  mbfmullem2  25787  mbfmul  25789  xrge0f  25794  itg2ge0  25798  itg2const  25803  itg2const2  25804  itg2uba  25806  itg2lea  25807  itg2splitlem  25811  itg2split  25812  itg2monolem1  25813  itg2mono  25816  itg2i1fseqle  25817  itg2i1fseq  25818  itg2addlem  25821  itg2gt0  25823  itg2cnlem1  25824  itg2cnlem2  25825  isibl2  25829  iblitg  25831  itgcl  25847  ibl0  25850  iblcnlem1  25851  itgcnlem  25853  iblss  25868  iblss2  25869  i1fibl  25871  itgitg1  25872  itgle  25873  itgeqa  25877  iblconst  25881  ibladdlem  25883  ibladd  25884  itgaddlem1  25886  itgfsum  25890  iblabslem  25891  iblabs  25892  iblabsr  25893  iblmulc2  25894  itgmulc2lem1  25895  itgsplit  25899  bddmulibl  25902  bddibl  25903  bddiblnc  25905  limccnp2  25955  limcco  25956  dvidlem  25978  dvcnp2  25983  dvaddbr  26001  dvmulbr  26002  dvaddf  26005  dvcmulf  26008  dvexp  26016  dvmptadd  26023  dvmptmul  26024  dvmptco  26035  dvmptfsum  26038  dvcnvlem  26039  dvef  26043  rolle  26053  mvth  26055  dvlip  26056  dvlipcn  26057  lhop1lem  26076  itgsubstlem  26111  itgpowd  26113  ply1divalg2  26200  uc1pmon1p  26213  q1pval  26216  r1pval  26219  elply2  26257  elplyr  26262  plypf1  26273  plyaddlem1  26274  coeeulem  26285  plyco  26302  coeaddlem  26310  coemulc  26316  dgradd2  26329  dgrcolem1  26334  dgrcolem2  26335  dgrco  26336  ofmulrt  26344  plymul02  26345  plymulidp  26347  plydivlem3  26360  plydivlem4  26361  plyrem  26370  iaa  26390  aareccl  26391  aannenlem2  26394  aaliou3lem3  26409  aaliou3lem7  26414  taylfval  26423  taylply2  26432  dvntaylp  26435  taylthlem2  26438  ulmclm  26451  ulmres  26452  ulmshftlem  26453  ulm0  26455  ulmcau  26459  ulmss  26461  ulmbdd  26462  ulmcn  26463  mtest  26468  mtestbdd  26469  iblulm  26471  itgulm  26472  pserulm  26486  pserdvlem2  26492  abelthlem5  26499  abelthlem6  26500  abelthlem8  26503  abelthlem9  26504  sincn  26508  coscn  26509  efcvx  26513  efabl  26616  logfac  26667  logcn  26713  chordthmlem  26898  chordthmlem5  26902  mcubic  26913  leibpi  27008  efrlim  27035  amgmlem  27055  lgamgulmlem2  27095  basellem7  27152  basellem9  27154  musum  27256  chtublem  27276  logexprlim  27290  dchrbas  27300  dchr1cl  27316  dchrabl  27319  dchrfi  27320  dchrhash  27336  bposlem6  27354  lgsdir2lem5  27394  gausslemma2dlem1  27431  lgseisenlem2  27441  lgseisenlem3  27442  lgseisenlem4  27443  lgsquad2lem2  27450  2lgslem1b  27457  2lgslem3b1  27466  2lgslem3c1  27467  2lgsoddprmlem4  27480  2sqlem8  27491  2sqlem11  27494  2sqreulem1  27511  2sqreunnlem1  27514  chtppilimlem2  27539  chebbnd2  27542  chpchtlim  27544  chpo1ub  27545  vmadivsum  27547  rpvmasumlem  27552  dchrisum0re  27578  dchrisum0  27585  mudivsum  27595  selberglem1  27610  selberglem2  27611  selberg2lem  27615  selberg2  27616  pntrsumo1  27630  selbergr  27633  abvcxp  27680  nosupfv  27771  noinffv  27786  madecut  27977  elons2  28352  oncutlt  28358  oniso  28365  seqsfn  28403  seqs1  28404  seqsp1  28405  n0fincut  28449  zcuts  28501  twocut  28517  expsval  28519  pw2cut2  28556  z12addscl  28571  z12shalf  28574  z12zsodd  28576  istrkgld  28629  istrkg2ld  28630  tgsegconeq  28656  tgbtwnouttr2  28665  ercgrg  28687  cgr3id  28689  tgbtwnxfr  28700  motgrp  28713  tgbtwnconn1lem3  28744  legov  28755  legid  28757  btwnleg  28758  legbtwn  28764  mirreu3  28828  mirinv  28840  miduniq1  28860  colmid  28862  krippenlem  28864  israg  28871  ragcgr  28881  motrag  28882  perpneq  28888  isperp2  28889  isperp2d  28890  footexALT  28892  footexlem1  28893  footexlem2  28894  foot  28896  perprag  28900  perpdragALT  28901  colperpexlem1  28904  mideulem2  28908  opphllem2  28922  opphllem3  28923  opphllem4  28924  midbtwn  28953  midcom  28956  mirmid  28957  lmieu  28958  lmif  28959  islmib  28961  lmilmi  28963  lmieq  28965  lmiinv  28966  lmiisolem  28970  hypcgrlem1  28973  hypcgrlem2  28974  lmiopp  28976  trgcopyeu  28980  plngval  28985  iscgra  29004  iscgra1  29005  iscgrad  29006  sacgr  29026  isinag  29033  isinagd  29034  inagflat  29035  inaghl  29040  isleag  29042  isleagd  29043  prlngref  29068  ttgval  29076  cchhllem  29088  usgredg4  29419  ushgredgedg  29431  ushgredgedgloop  29433  usgrstrrepe  29437  uspgr1e  29446  uhgrspan1  29505  usgrres1  29517  nbgrnself  29561  nbusgredgeu  29568  cusgrfilem2  29658  finsumvtxdg2size  29752  finsumvtxdgeven  29754  wlk1walk  29840  uspgr2wlkeq  29847  uspgr2wlkeqi  29849  wlkonwlk  29862  wlkonwlk1l  29863  usgr2trlncl  29961  crctcshwlkn0lem7  30017  wwlksnredwwlkn  30096  wwlksnextbij  30103  wwlksnextprop  30113  wwlksnwwlksnon  30116  elwwlks2ons3im  30155  clwlkclwwlk2  30206  clwlkclwwlkfo  30212  clwlkclwwlkf1  30213  clwwlkwwlksb  30257  clwlknf1oclwwlkn  30287  clwwlknonmpo  30292  clwwlknonex2lem2  30311  0pthon1  30331  uhgr3cyclex  30385  iseupth  30404  eupth0  30417  eupth2lem2  30422  frgr3vlem1  30476  3vfriswmgrlem  30480  2clwwlk2clwwlklem  30549  wlkl0  30570  numclwlk1lem2  30573  grpodivfval  30738  dipfval  30906  ipval2  30911  lnoval  30956  minvecolem3  31080  h2hcau  31183  h2hlm  31184  opsqrlem3  32346  opsqrlem4  32347  foresf1o  32704  disjnf  32771  disjdifprg  32776  iundisjf  32790  br8d  32811  fnfvor  32812  ofrco  32813  ofrn2  32843  off2  32844  ofresid  32845  fmptcof2  32860  aciunf1  32866  ofpreima  32868  f1ocnt  33003  prodindf  33041  indf1ofs  33045  wrdfsupp  33116  wrdpmcl  33117  pfxf1  33121  s1f1  33122  wrdt2ind  33132  swrdrn2  33133  ressnm  33143  abvpropd2  33144  ismntd  33163  dfmgc2lem  33174  pwrssmgc  33179  gsummpt2d  33230  gsummptf1od  33236  gsummptfsf1o  33241  gsumhashmul  33248  gsumwrd2dccat  33259  wrdpmtrlast  33274  psgnfzto1stlem  33281  fzto1st1  33283  tocycfv  33290  cycpmcl  33297  tocycf  33298  tocyc01  33299  cycpmco2f1  33305  cycpmco2rn  33306  cycpmco2lem1  33307  cycpmco2lem2  33308  cycpmco2lem3  33309  cycpmco2lem4  33310  cycpmco2lem5  33311  cycpmco2lem6  33312  cycpmco2lem7  33313  cycpmco2  33314  cycpm3cl2  33317  cycpmconjv  33323  tocyccntz  33325  cyc3evpm  33331  cyc3genpm  33333  cycpmgcl  33334  cycpmconjslem2  33336  cyc3conja  33338  sgnsv  33341  inftmrel  33361  isinftm  33362  submarchi  33367  isslmd  33383  urpropd  33412  elrgspnlem1  33424  elrgspnlem2  33425  elrgspnlem4  33427  elrgspn  33428  elrgspnsubrun  33431  erlval  33440  rlocval  33441  rlocbas  33450  rlocaddval  33451  rlocmulval  33452  rloccring  33453  rlocinvunit  33457  rlocisunit  33458  resv0g  33525  resvcmn  33527  imaslmod  33540  imasmhm  33541  imasghm  33542  imasrhm  33543  imaslmhm  33544  znfermltl  33553  islinds5  33554  ellspds  33555  linds2eq  33568  lindfpropd  33569  elringlsmd  33581  nsgmgclem  33598  nsgmgc  33599  rhmquskerlem  33612  elrspunsn  33616  idlinsubrg  33618  qsidomlem1  33640  qsidomlem2  33641  opprqusbas  33677  qsdrngi  33684  dflring2  33690  rprmval  33713  rprmnz  33717  rprmnunit  33718  unitmulrprm  33725  1arithidomlem1  33732  1arithidomlem2  33733  1arithidom  33734  1arithufdlem3  33743  dfufd2lem  33746  ply1dg1rt  33777  ply1mulrtss  33779  ply1degltlss  33793  ply1gsumz  33796  r1pquslmic  33808  0mplrim  33812  selvply1rhmlemb  33817  selvply1rhmlem2  33819  selvply1rhmlem4  33821  mplvrpmfgalem  33842  psrmonprod  33850  esplyfvaln  33872  esplyind  33873  vietalem  33877  sra1r  33879  sradrng  33880  sraidom  33881  srasubrg  33882  resssra  33885  drgext0g  33888  drgextlsp  33892  rlmdim  33908  tnglvec  33910  tngdim  33911  matdim  33913  ply1degltdimlem  33920  lbsdiflsp0  33924  dimkerim  33925  fedgmullem2  33928  lactlmhm  33932  extdg1id  33964  ccfldsrarelvec  33969  ccfldextdgrr  33970  fldextrspunlsplem  33971  fldextrspunlsp  33972  fldextrspunlem1  33973  fldextrspunfld  33974  fldextrspunlem2  33975  extdgfialglem1  33990  extdgfialglem2  33991  irredminply  34014  algextdeglem3  34017  algextdeglem4  34018  algextdeglem8  34022  constrsslem  34039  constrext2chnlem  34048  constrcon  34072  2sqr3nconstr  34079  cos9thpinconstrlem2  34088  1smat1  34102  submatres  34104  submateq  34107  lmatcl  34114  mdetlap1  34124  madjusmdetlem3  34127  circtopn  34135  locfinref  34139  tpr2rico  34210  lmdvglim  34252  qqhval  34270  esumeq1  34332  esumeq1d  34333  esumeq2d  34335  esumf1o  34348  esumsplit  34351  esumadd  34355  gsumesum  34357  esumlub  34358  esumaddf  34359  esumcst  34361  esumsnf  34362  esumpinfval  34371  esumcocn  34378  esummulc1  34379  esumcvg  34384  esum2d  34391  ofcval  34397  ofcfn  34398  ofcfeqd2  34399  ofcf  34401  ofcfval4  34403  ofcof  34405  sigapildsys  34460  sxval  34488  measvunilem0  34511  measvuni  34512  measiun  34516  meascnbl  34517  measinb  34519  volmeas  34529  sxbrsiga  34588  omssubadd  34598  fiunelcarsg  34614  itgeq12dv  34624  sitgval  34630  eulerpartlems  34658  eulerpartgbij  34670  eulerpartlemn  34679  sseqf  34690  sseqp1  34693  totprobd  34724  probfinmeasb  34726  probmeasb  34728  rrvadd  34750  dstfrvclim1  34776  gsumnunsn  34839  signsply0  34846  fdvneggt  34895  fdvnegge  34897  itgexpif  34901  reprpmtf1o  34921  circlemethhgt  34938  logdivsqrle  34945  hgt750lemg  34949  hgt750lemb  34951  hgt750lema  34952  f1resfz0f1d  35465  2cycl2d  35490  quartfull  35516  sconnpi1  35590  cvmliftphtlem  35668  cvmlift3lem2  35671  satfv1  35714  satfdmlem  35719  satf0suc  35727  satf0op  35728  sat1el2xp  35730  fmla  35732  fmlasuc0  35735  fmlafvel  35736  fmlasuc  35737  fmla1  35738  satffunlem1lem2  35754  satffunlem2lem2  35757  sategoelfvb  35770  satfv1fvfmla1  35774  2goelgoanfmla1  35775  elmsubrn  35879  msubco  35882  mthmpps  35933  r1peuqusdeg1  35994  sinccvg  36024  circum  36025  br8  36107  br4  36109  brsegle  36459  hilbert1.1  36505  itgeq2sdv  36581  ditgeq3sdv  36584  cbvoprab23davw  36637  cbvoprab13davw  36638  trer  36677  knoppcnlem4  36935  knoppcnlem9  36940  knoppcnlem11  36942  knoppndvlem6  36956  knoppf  36974  bj-imdirco  37683  bj-fvmptunsn2  37751  bj-finsumval0  37778  exrecfnlem  37874  finxpreclem1  37884  matunitlindflem1  38116  matunitlindflem2  38117  poimirlem1  38121  poimirlem2  38122  poimirlem4  38124  poimirlem5  38125  poimirlem6  38126  poimirlem7  38127  poimirlem10  38130  poimirlem11  38131  poimirlem12  38132  poimirlem16  38136  poimirlem17  38137  poimirlem19  38139  poimirlem20  38140  poimirlem22  38142  poimirlem23  38143  poimirlem28  38148  poimirlem29  38149  poimirlem31  38151  broucube  38154  mblfinlem2  38158  volsupnfl  38165  itg2addnclem  38171  itg2addnclem3  38173  itg2addnc  38174  itg2gt0cn  38175  ibladdnclem  38176  itgaddnclem1  38178  itgaddnc  38180  iblabsnclem  38183  iblabsnc  38184  iblmulc2nc  38185  itgmulc2nclem1  38186  itgmulc2nclem2  38187  itgmulc2nc  38188  ftc1anclem2  38194  ftc1anclem4  38196  ftc1anclem5  38197  ftc1anclem6  38198  ftc1anclem7  38199  ftc1anclem8  38200  ftc1anc  38201  areacirc  38213  unirep  38214  upixp  38229  sdc  38244  lmclim2  38258  geomcau  38259  caures  38260  caushft  38261  prdsbnd2  38295  heibor1lem  38309  bfplem2  38323  rrncmslem  38332  isrngo  38397  iuneq2f  38656  dmec2d  38811  lflset  39684  islfld  39687  lfladdcl  39696  lflvscl  39702  lkrsc  39722  eqlkr2  39725  lshpkrlem1  39735  ldualset  39750  ldualvaddval  39756  ldualvsval  39763  ldualgrplem  39770  lduallmodlem  39777  cmtfvalN  39835  isoml  39863  iscvlat  39948  llni2  40137  lplni2  40162  lvoli3  40202  lvoli2  40206  paddfval  40422  lhpset  40620  ltrnfset  40742  trlfset  40785  cdleme21k  40963  cdlemeiota  41210  tgrpfset  41369  tgrpset  41370  tgrpabl  41376  tendo0cbv  41411  tendo02  41412  erngfset  41424  erngset  41425  erngfset-rN  41432  erngset-rN  41433  cdlemkid5  41560  cdlemkid  41561  dvafset  41629  dvaset  41630  diaffval  41655  dialss  41671  diaf11N  41674  dvhfset  41705  dvhset  41706  docaffvalN  41746  dibfval  41766  dibf11N  41786  diblss  41795  diclss  41818  dihord2cN  41846  dihord11b  41847  dihffval  41855  dihord6apre  41881  dihglblem2aN  41918  dihglblem2N  41919  dihjatcclem4  42046  lclkrs  42164  mapdh6dN  42364  mapdh6eN  42365  mapdh6fN  42366  mapdh6jN  42370  hvmapffval  42383  hvmapfval  42384  mapdh8a  42400  mapdh8ad  42404  mapdh8d0N  42407  mapdh8d  42408  mapdh8i  42411  mapdh8j  42412  mapdh9a  42414  mapdh9aOLDN  42415  hdmap1l6d  42438  hdmap1l6e  42439  hdmap1l6f  42440  hdmap1l6j  42444  hdmapval2  42457  hdmapeveclem  42459  hdmapval3lemN  42462  hdmap11lem1  42466  hgmapfval  42511  hlhils0  42570  hlhils1N  42571  hlhillvec  42576  hlhildrng  42577  hlhil0  42580  hlhillsm  42581  rhmzrhval  42590  zndvdchrrhm  42591  3factsumint1  42639  lcmineqlem12  42658  aks4d1p1p4  42689  aks4d1p1p7  42692  aks4d1p9  42706  isprimroot  42711  primrootsunit1  42715  posbezout  42718  primrootscoprbij  42720  remexz  42722  aks6d1c1p2  42727  aks6d1c1p3  42728  aks6d1c1p4  42729  aks6d1c1p5  42730  aks6d1c1p7  42731  evl1gprodd  42735  aks6d1c2p2  42737  hashscontpow  42740  aks6d1c2lem4  42745  aks6d1c2  42748  aks6d1c5lem2  42756  aks6d1c5  42757  deg1gprod  42758  2np3bcnp1  42762  2ap1caineq  42763  sticksstones8  42771  sticksstones10  42773  sticksstones12a  42775  sticksstones12  42776  sticksstones17  42781  sticksstones18  42782  sticksstones19  42783  sticksstones21  42785  sticksstones22  42786  aks6d1c6lem1  42788  aks6d1c6lem2  42789  aks6d1c6lem4  42791  aks6d1c6isolem1  42792  aks5lem3a  42807  grpods  42812  unitscyglem1  42813  unitscyglem2  42814  ofun  42855  redivcan2d  43057  redivcan3d  43058  sn-rediv0d  43063  sn-redividd  43064  rhmpsr1  43167  evlselv  43172  fsuppind  43173  mhphf  43180  3cubeslem3r  43269  eldiophb  43339  eldioph  43340  eldioph3  43348  rabren3dioph  43393  pellqrexplicit  43455  rmxycomplete  43495  rmxynorm  43496  acongrep  43558  jm2.26a  43578  jm2.26  43580  fnwe2lem2  43629  fnwe2lem3  43630  aomclem5  43636  aomclem8  43639  imasgim  43678  isnumbasgrplem1  43679  hbtlem5  43706  dgrsub2  43713  rgspnid  43746  rngunsnply  43747  mendval  43757  mendring  43766  mendlmod  43767  mendassa  43768  nnoeomeqom  43890  tfsconcatb0  43922  oaun3  43960  safesnsupfilb  43995  fsovrfovd  44586  fsovcnvlem  44590  mnring0gd  44798  mnringlmodd  44803  mnringmulrcld  44805  colleq1  44831  colleq2  44832  dvgrat  44889  radcnvrat  44891  hashnzfzclim  44899  caofcan  44900  ofsubid  44901  ofmul12  44902  ofdivrec  44903  ofdivcan4  44904  ofdivdiv2  44905  expgrowth  44912  binomcxplemnn0  44926  binomcxplemrat  44927  binomcxplemdvbinom  44930  binomcxplemnotnn0  44933  wessf1ornlem  45764  disjf1o  45770  ssnnf1octb  45773  mapss2  45783  icof  45796  mpteq1df  45812  infnsuprnmpt  45826  upbdrech  45885  divcan8d  45892  dmmcand  45893  suplesup  45916  ssuzfz  45926  supsubc  45930  xralrple2  45931  fprodabs2  46172  fprodcn  46177  clim1fr1  46178  climrec  46180  climexp  46182  climinf  46183  climsuse  46185  climneg  46187  divcnvg  46204  sumnnodd  46207  clim2f  46211  clim2f2  46245  fnlimfvre  46249  climleltrp  46251  climreclmpt  46259  climinf2mpt  46289  climinfmpt  46290  supcnvlimsup  46315  climuzlem  46318  climisp  46321  climrescn  46323  climxrrelem  46324  climxrre  46325  liminfvalxrmpt  46361  liminflbuz2  46390  cncfcompt  46458  dvsinax  46488  fperdvper  46494  dvcosax  46501  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  dvnxpaek  46517  dvnmul  46518  dvmptfprodlem  46519  dvnprodlem1  46521  dvnprodlem2  46522  dvnprodlem3  46523  iblempty  46540  iblsplit  46541  itgcoscmulx  46544  itgsincmulx  46549  itgsubsticc  46551  sublevolico  46559  stoweidlem2  46577  stoweidlem17  46592  stoweidlem21  46596  stoweidlem32  46607  stoweidlem46  46621  stoweidlem55  46630  wallispi  46645  wallispi2lem1  46646  wallispi2lem2  46647  wallispi2  46648  stirlinglem3  46651  dirkercncflem2  46679  dirkercncflem4  46681  fourierdlem16  46698  fourierdlem18  46700  fourierdlem21  46703  fourierdlem22  46704  fourierdlem39  46721  fourierdlem53  46734  fourierdlem58  46739  fourierdlem59  46740  fourierdlem62  46743  fourierdlem73  46754  fourierdlem76  46757  fourierdlem81  46762  fourierdlem83  46764  fourierdlem93  46774  fourierdlem101  46782  fourierdlem103  46784  fourierdlem104  46785  fourierdlem111  46792  fourierdlem112  46793  fouriersw  46806  elaa2lem  46808  etransclem18  46827  etransclem32  46841  etransclem33  46842  etransclem46  46855  etransclem48  46857  rrxtopnfi  46862  rrxunitopnfi  46867  salincl  46899  sge0z  46950  sge0tsms  46955  sge0snmpt  46958  sge0sup  46966  sge0resplit  46981  sge0ss  46987  sge0isum  47002  sge0xp  47004  sge0xaddlem2  47009  sge0seq  47021  sge0reuzb  47023  meadjun  47037  meadjiun  47041  ismeannd  47042  meaiunlelem  47043  meaiininclem  47061  caragenunidm  47083  caragenuncllem  47087  omeiunltfirp  47094  carageniuncllem1  47096  caratheodorylem1  47101  0ome  47104  isomenndlem  47105  hoicvr  47123  hoicvrrex  47131  ovn0lem  47140  ovn0  47141  ovnsubaddlem1  47145  hoidmvval0  47162  hoidmvval0b  47165  hoidmv1lelem1  47166  hoidmv1le  47169  hoidmvlelem2  47171  hoidmvlelem3  47172  hoidmvlelem4  47173  hoidmvlelem5  47174  ovnhoilem1  47176  ovnhoilem2  47177  ovnhoi  47178  dmvon  47181  hspval  47184  ovnlecvr2  47185  hoiqssbllem2  47198  hspmbllem2  47202  hspmbl  47204  hoimbl  47206  ovnsubadd2lem  47220  ovolval4lem1  47224  ovnovollem1  47231  vonvolmbl  47236  vonvol2  47239  iccvonmbllem  47253  vonioolem2  47256  vonn0ioo2  47265  vonn0icc2  47267  smfpimltmpt  47321  issmfdmpt  47323  smfconst  47324  smfpimltxrmptf  47333  smflimlem2  47347  smflimlem3  47348  smflim  47352  smfpimgtmpt  47356  smfpimgtxrmptf  47359  smfsupmpt  47390  smfinfmpt  47394  smflimsuplem4  47398  fresfo  47643  fsetsnf  47646  fsetsnprcnex  47650  cfsetsnfsetf  47653  cfsetsnfsetfo  47655  3f1oss1  47670  f1cof1b  47672  funfocofob  47673  afveq1  47729  afveq2  47730  afvco2  47771  rspceaov  47792  faovcl  47795  afv2eq12d  47810  afv2eq1  47811  afv2eq2  47812  dfatcolem  47850  f1oresf1orab  47884  preimafvsnel  47986  preimafvelsetpreimafv  47995  fundcmpsurbijinjpreimafv  48014  fundcmpsurinjimaid  48018  fundcmpsurinjALT  48019  ichnreuop  48079  ichreuopeq  48080  prelspr  48093  sprsymrelf1lem  48098  sprsymrelfolem2  48100  prproropreud  48116  reuopreuprim  48133  fmtnofac2lem  48178  proththd  48224  requad01  48244  dfodd6  48260  nnsum3primesprm  48413  clnbgrvtxel  48452  isgrim  48505  grimid  48509  upgrimtrls  48529  isubgrgrim  48552  clnbgrgrim  48557  usgrgrtrirex  48573  stgrnbgr0  48587  isubgr3stgrlem6  48594  isgrlim  48605  uspgrlim  48615  grlimedgclnbgr  48618  grlimgrtri  48626  grilcbri2  48634  gpgedgiov  48688  gpg5gricstgr3  48713  gpg5grlim  48716  grlimedgnedg  48754  uspgrsprfo  48771  copissgrp  48791  copisnmnd  48792  isasslaw  48815  2zrngamgm  48868  cznrng  48884  rngcvalALTV  48888  rngcbasALTV  48889  rngchomfvalALTV  48890  rngccofvalALTV  48893  rngccoALTV  48894  rngccatidALTV  48895  rhmsubcALTV  48908  ringcvalALTV  48912  ringcbasALTV  48923  ringchomfvalALTV  48924  ringccofvalALTV  48927  ringccoALTV  48928  ringccatidALTV  48929  scmsuppss  48994  ply1mulgsum  49013  dflinc2  49033  lcoop  49034  lincvalsng  49039  lincvalpr  49041  lincvalsc0  49044  lcoc0  49045  lcoel0  49051  lincsum  49052  lincolss  49057  islininds  49069  lindslinindsimp1  49080  lindsrng01  49091  snlindsntorlem  49093  lincresunit3  49104  islindeps2  49106  lmod1lem3  49112  lmod1zr  49116  itcoval  49284  itcoval0  49285  itcoval1  49286  itcoval2  49287  itcoval3  49288  itcovalsuc  49290  itcovalsucov  49291  itcovalendof  49292  itcovalpclem2  49294  itcovalt2lem2  49299  ackvalsuc1mpt  49301  ackval1  49304  ackval2  49305  ackval3  49306  ackvalsucsucval  49311  affinecomb1  49325  rrx2plordisom  49346  lines  49354  line  49355  rrxline  49357  spheres  49369  line2xlem  49376  itsclc0yqsol  49387  itscnhlinecirc02p  49408  fmpod  49492  iscnrm3llem1  49571  iscnrm3llem2  49572  iscnrm3l  49573  glbsscl  49583  posjidm  49594  posmidm  49595  toslat  49604  ipolubdm  49609  ipoglbdm  49612  mreclat  49619  topclat  49620  iinfssc  49679  iinfsubc  49680  infsubc2  49683  iinfconstbas  49688  nelsubc3  49693  initc  49713  funchomf  49719  imaidfu2lem  49731  imaidfu  49732  imaidfu2  49733  cofidf2  49742  funcoppc4  49766  fthcomf  49779  idfth  49780  idsubc  49782  upciclem1  49788  upfval2  49799  upfval3  49800  isuplem  49801  oppcup3lem  49828  uobffth  49840  uobeqw  49841  uptr2  49843  initopropd  49865  termopropd  49866  dfswapf2  49883  swapfelvv  49885  swapf1vala  49888  swapf2fn  49890  swapf2  49896  tposcurf1cl  49918  tposcurf11  49919  tposcurf12  49920  tposcurf1  49921  tposcurf2  49922  tposcurf2val  49923  tposcurf2cl  49924  tposcurfcl  49925  fucoelvv  49942  fucofvalne  49947  fuco11  49948  fuco11cl  49949  fuco21  49958  fuco11b  49959  fuco11bALT  49960  fuco22natlem3  49966  fuco22natlem  49967  fuco23a  49974  fucofunc  49981  fucofunca  49982  fucolid  49983  fucorid  49984  postcofval  49986  precofval  49989  precofvalALT  49990  precoffunc  49994  prcofelvv  50002  reldmprcof1  50003  reldmprcof2  50004  prcoftposcurfuco  50005  prcoffunc  50007  prcoffunca  50008  fucoppcco  50031  fucoppccic  50035  oppfdiag1  50036  oppfdiag1a  50037  isthincd2lem1  50047  oppcthin  50060  oppcthinco  50061  subthinc  50065  fullthinc  50072  thincciso2  50077  indthinc  50084  prsthinc  50086  setcthin  50087  setc2othin  50088  setcsnterm  50112  setc1ocofval  50116  isinito2lem  50120  dfinito4  50123  idfudiag1  50147  arweuthinc  50151  diag1f1olem  50155  prstchomval  50181  prstcprs  50182  prstcthin  50183  prstchom2  50185  oduoppcciso  50188  postcpos  50189  postcposALT  50190  postc  50191  mndtccatid  50209  mndtcid  50211  oppgoppchom  50212  oppgoppcco  50213  oppgoppcid  50214  grptcmon  50215  grptcepi  50216  2arwcat  50222  lanfval  50235  ranfval  50236  lanpropd  50237  ranpropd  50238  rellan  50245  lanrcl5  50257  ranrcl5  50262  lanup  50263  ranup  50264  lmdfval  50271  cmdfval  50272  lmdpropd  50279  cmdpropd  50280  concom  50285  coccom  50286  islmd  50287  iscmd  50288  lmddu  50289  termolmd  50292  lmdran  50293  cmdlan  50294  aacllem  50423  amgmwlem  50424