Theorem eqidd 2737

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 2736	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  nfabd2  2922  neleq1  3042  neleq2  3043  cbvraldvaOLD  3320  cbvrexdvaOLD  3321  rspcedeq1vd  3583  rspcedeq2vd  3584  elabd3  3625  nelrdva  3663  sbcbidv  3796  csbie2df  4395  reusngf  4631  rexreusng  4636  reuprg0  4659  iunxdif3  5050  mpteq1  5187  mpteq1i  5189  mpteq2da  5190  mpteq2dva  5191  nfcvb  5321  dfid2  5521  feq23d  6657  f10d  6808  fvmptdv2  6959  elrnrexdm  7034  f1ossf1o  7073  fmptco  7074  cofmpt  7077  fprg  7100  ftpg  7101  fmptsng  7114  fmptsnd  7115  f1dom3fv3dif  7214  f1dom3el3dif  7215  fliftfun  7258  fliftval  7262  nfriotad  7326  cbvmpo  7452  fconstmpo  7475  eqfnov2  7488  ovmpod  7510  ovmpodv2  7516  fvmpopr2d  7520  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ovmpt3rab1  7616  elovmpt3rab  7619  ofval  7633  ofrval  7634  offn  7635  fnfvof  7639  off  7640  ofres  7641  coof  7646  ofco  7647  caofref  7653  caofid0l  7655  caofid0r  7656  caofid1  7657  caofid2  7658  caofrss  7661  caoftrn  7663  tfisi  7801  fsplitfpar  8060  fczsupp0  8135  suppssof1  8141  suppofss1d  8146  suppofss2d  8147  fvmpocurryd  8213  fpr3g  8227  iserd  8661  fsetfocdm  8798  ixpsnf1o  8876  mapxpen  9071  dffi3  9334  cantnf0  9584  cantnfp1  9590  cantnflem1  9598  ttrcltr  9625  axcclem  10367  ttukeylem3  10421  fpwwe2lem8  10549  ofsubeq0  12142  ofnegsub  12143  ofsubge0  12144  fzo0to3tp  13668  fzo1to4tp  13670  modsubmod  13852  seqid  13970  seqid2  13971  seqz  13973  seqof  13982  elovmptnn0wrd  14482  ccatdmss  14505  ccatws1ls  14557  pfxsuffeqwrdeq  14621  wrdind  14645  wrd2ind  14646  ccats1pfxeqbi  14665  repswsymb  14697  repswsymball  14702  repswsymballbi  14703  s3eq2  14793  swrds2m  14864  wrdl2exs2  14869  swrd2lsw  14875  wwlktovfo  14881  s3sndisj  14890  s3iunsndisj  14891  relexp0g  14945  relexpsucnnr  14948  relexp1g  14949  rtrclreclem1  14980  rtrclreclem4  14984  dfrtrcl2  14985  rlim2  15419  climcl  15422  rlimcl  15426  clim2  15427  rlimclim1  15468  rlimclim  15469  climrlim2  15470  climuni  15475  rlimres  15481  climeq  15490  2clim  15495  climshftlem  15497  climabs0  15508  climcn1  15515  climcn2  15516  o1of2  15536  o1rlimmul  15542  o1add2  15547  o1mul2  15548  o1sub2  15549  o1dif  15553  climsqz  15564  climsqz2  15565  rlimdiv  15569  isercoll  15591  climsup  15593  climcau  15594  caurcvgr  15597  caucvgb  15603  serf0  15604  iseralt  15608  sumz  15645  fsumss  15648  fsumsplitsn  15667  fsumsplit1  15668  fsumsplitsnun  15678  isumclim3  15682  isummulc2  15685  fsum2dlem  15693  fsumconst  15713  fsumabs  15724  fsumparts  15729  fsumrlim  15734  fsumo1  15735  seqabs  15737  cvgcmpce  15741  fsumiun  15744  ackbijnn  15751  isumshft  15762  isumltss  15771  climcndslem1  15772  climcndslem2  15773  climcnds  15774  mertenslem1  15807  mertenslem2  15808  prod1  15867  fprodss  15871  fprodconst  15901  fprod2dlem  15903  fprodsplitsn  15912  iprodclim3  15923  eftlcl  16032  reeftlcl  16033  eftlub  16034  efsep  16035  effsumlt  16036  eirrlem  16129  rpnnen2lem6  16144  rpnnen2lem7  16145  rpnnen2lem8  16146  rpnnen2lem9  16147  rpnnen2lem12  16150  2tp1odd  16279  sadasslem  16397  smupvallem  16410  smumul  16420  alginv  16502  algfx  16507  cncongr1  16594  qnumdencoprm  16672  qeqnumdivden  16673  vdwlem1  16909  vdwlem12  16920  vdwlem13  16921  prmodvdslcmf  16975  prmgap  16987  prmgaplcm  16988  prmgapprmo  16990  setsexstruct2  17102  setsstruct  17103  prdssca  17376  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdsip  17381  prdsle  17382  prdsds  17384  prdstset  17386  prdshom  17387  prdsco  17388  prdsvscafval  17400  prdsdsval2  17404  prdsdsval3  17405  pwsle  17413  pwsleval  17414  pwsvscaval  17416  imasbas  17433  imasds  17434  imasplusg  17438  imasmulr  17439  imassca  17440  imasvsca  17441  imasip  17442  imastset  17443  imasle  17444  imasvscafn  17458  imasvscaval  17459  qusin  17465  xpsvsca  17498  iscat  17595  iscatd  17596  iscatd2  17604  0catg  17611  homfeq  17617  homfeqd  17618  comfffval2  17624  comffval2  17625  comfeq  17629  comfeqd  17630  oppccatid  17642  2oppccomf  17648  moni  17660  rcaninv  17718  ssc2  17746  ssctr  17749  ssceq  17750  subcssc  17764  subccat  17772  subsubc  17777  funcres  17820  funcres2  17822  idfusubc  17824  funcres2c  17827  idffth  17859  cofull  17860  cofth  17861  ressffth  17864  isnat  17874  fuccofval  17886  fuccatid  17896  fucpropd  17904  elhomai  17957  coafval  17988  setcval  18001  setcbas  18002  setchomfval  18003  setccofval  18006  setcco  18007  setccatid  18008  setcepi  18012  funcsetcres2  18017  catcval  18024  catcbas  18025  catchomfval  18026  catccofval  18028  catcco  18029  catccatid  18030  catcfuccl  18042  estrcval  18047  estrcbas  18048  estrchomfval  18049  estrccofval  18052  estrcco  18053  estrccatid  18055  estrreslem2  18061  fullestrcsetc  18074  fullsetcestrc  18089  xpcbas  18101  xpchomfval  18102  xpccofval  18105  xpccatid  18111  prfval  18122  catcxpccl  18130  xpcpropd  18131  evlfval  18140  curfval  18146  curf1  18148  curf12  18150  curf2  18152  curf2val  18153  hofval  18175  hof2fval  18178  hofcllem  18181  oppchofcl  18183  oppcyon  18192  oyoncl  18193  yonedalem4a  18198  yonedalem4b  18199  yonedainv  18204  oduposb  18250  joinval  18298  meetval  18312  isdlat  18445  ipopos  18459  pfxchn  18533  chnind  18544  chnso  18547  chnccats1  18548  chnccat  18549  chnrev  18550  gsumpropd  18603  gsumpropd2lem  18604  gsumval1  18608  gsumval2a  18610  issgrp  18645  issgrpd  18655  prdssgrpd  18658  ismndd  18681  mndprop  18685  prdsmndd  18695  imasmnd2  18699  insubm  18743  mhmima  18750  frmdbas  18777  frmdmnd  18784  efmnd  18795  smndex1gid  18828  smndex1n0mnd  18837  smndex2dlinvh  18842  sgrpnmndex  18857  resgrpplusfrn  18880  grpprop  18882  grpsubfval  18913  grpsubfvalALT  18914  grpsubpropd  18975  prdsgrpd  18980  imasgrp2  18985  imasgrp  18986  imasgrpf1  18987  mulgfval  18999  mulgfvalALT  19000  mulgnngsum  19009  mulgnn0gsum  19010  mulgpropd  19046  subgsub  19068  eqgfval  19105  qusgrp  19115  ghmqusnsglem1  19209  ghmqusnsglem2  19210  ghmqusnsg  19211  ghmquskerlem1  19212  ghmquskerlem2  19214  ghmquskerlem3  19215  ghmqusker  19216  oppgmnd  19283  oppgmndb  19284  oppggrp  19286  oppggrpb  19287  symgval  19300  symg1bas  19320  symg2bas  19322  symgvalstruct  19326  symggrp  19329  gsmsymgrfixlem1  19356  gsmsymgreqlem2  19360  symgfixels  19363  symgsssg  19396  symgfisg  19397  psgnunilem4  19426  psgnvalii  19438  oppglsm  19571  lsmelvalmi  19581  efgi0  19649  efgi1  19650  efgtf  19651  efgval2  19653  efginvrel2  19656  frgp0  19689  frgpup3lem  19706  ablprop  19722  subcmn  19766  gex2abl  19780  prdscmnd  19790  qusabl  19794  abl1  19795  cygabl  19820  gsumzf1o  19841  gsumzaddlem  19850  gsumzsplit  19856  gsumconst  19863  gsumconstf  19864  gsummptshft  19865  gsummhm2  19868  gsummptmhm  19869  gsumzunsnd  19885  gsumunsnfd  19886  gsumpt  19891  gsummptf1o  19892  gsummptun  19893  gsum2dlem2  19900  gsumcom2  19904  nn0gsumfz  19913  dprdval  19934  dprdssv  19947  dprdfeq0  19953  dprdsubg  19955  dprdspan  19958  dprdz  19961  subgdmdprd  19965  subgdprd  19966  gsumle  20074  isrng  20089  isrngd  20108  prdsrngd  20111  imasrng  20112  issrg  20123  isring  20172  ringabl  20216  ringprop  20225  isringd  20226  prdsringd  20256  prdscrngd  20257  prds1  20258  pwspjmhmmgpd  20263  imasring  20266  opprrng  20281  opprrngb  20282  opprringb  20284  dvrfval  20338  rnghmf1o  20388  c0mgm  20395  c0mhm  20396  c0snmgmhm  20398  c0snmhm  20399  rngisomring1  20404  rhmf1o  20426  pwsco1rhm  20435  pwsco2rhm  20436  zrrnghm  20469  rhmimasubrng  20499  pwsdiagrhm  20540  rngcbas  20554  rngchomfval  20555  dfrngc2  20561  rnghmsscmap2  20562  rnghmsscmap  20563  rngccat  20567  rngcid  20568  funcrngcsetc  20573  funcrngcsetcALT  20574  zrinitorngc  20575  zrtermorngc  20576  ringcbas  20583  ringchomfval  20584  dfringc2  20590  rhmsscmap2  20591  rhmsscmap  20592  ringccat  20596  ringcid  20597  rngcresringcat  20602  funcringcsetc  20607  zrtermoringc  20608  rhmsubc  20622  drngprop  20677  isdrngd  20698  isdrngrd  20699  isdrngdOLD  20700  isdrngrdOLD  20701  abvtrivd  20765  idsrngd  20789  suborng  20809  islmodd  20817  lmodabl  20860  lss1  20889  lsssn0  20899  islss3  20910  lss1d  20914  lssintcl  20915  prdslmodd  20920  idlmhm  20993  invlmhm  20994  lmhmvsca  20997  lbsextlem2  21114  sralmod  21139  sralmod0  21140  rlm0  21147  rlmvneg  21158  rnglidlmsgrp  21201  rnglidlrng  21202  qus2idrng  21228  crngridl  21235  quscrng  21238  rhmqusnsg  21240  rngqiprngimf1lem  21249  rngqiprngimf1  21255  dfcnfldOLD  21325  absabv  21379  pzriprnglem10  21445  zrhpropd  21469  fermltlchr  21484  znzrh  21497  znbas  21498  zncrng  21499  znzrhfo  21502  znf1o  21506  frgpcyg  21528  evpmodpmf1o  21551  isphld  21609  phlpropd  21610  phssip  21613  phlssphl  21614  pjfval  21661  dsmmval  21689  dsmmsubg  21698  frlmip  21733  frlmipval  21734  frlmphllem  21735  frlmphl  21736  islindf  21767  islindf4  21793  isassa  21811  isassad  21820  issubassa3  21821  sraassaOLD  21825  asclfval  21834  ressascl  21852  psrval  21871  psrbaglesupp  21878  psrbagcon  21881  psrbaglefi  21882  psrbagleadd1  21884  psrbagconf1o  21885  gsumbagdiaglem  21886  psrass1lem  21888  psrbas  21889  psrplusg  21892  psrmulr  21898  psrsca  21903  psrvscafval  21904  psrvscaval  21906  psrlmod  21915  psrlidm  21917  psrdi  21920  psrdir  21921  psrcom  21923  psrring  21925  psrassa  21928  mplsubglem  21954  mpllsslem  21955  mplvscaval  21971  mplcoe1  21992  mplcoe3  21993  mplcoe5  21995  opsrcrng  22014  opsrassa  22015  mplmon2  22016  evlslem2  22034  evlslem1  22037  evlsvvval  22048  mhpmulcl  22092  psdffval  22100  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  ply1lss  22137  ply1subrg  22138  opsr0  22159  opsr1  22160  subrgply1  22173  psrplusgpropd  22176  psropprmul  22178  opsrring  22185  opsrlmod  22186  ply1mpl0  22197  ply1mpl1  22199  coe1z  22205  coe1mul2  22211  coe1tm  22215  coe1sclmulfv  22225  ply1coe  22242  evls1rhm  22266  evls1sca  22267  evl1rhm  22276  evl1sca  22278  evl1expd  22289  evl1gsumdlem  22300  evl1varpw  22305  evls1maplmhm  22321  mamufval  22336  mamudi  22347  mamudir  22348  mat0  22361  matinvg  22362  matlmod  22373  matinvgcell  22379  matring  22387  matassa  22388  mat0dimcrng  22414  mat1dim0  22417  mat1f1o  22422  dmatmulcl  22444  scmatval  22448  scmatscmiddistr  22452  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  scmatlss  22469  scmatrhmcl  22472  1mavmul  22492  mavmul0  22496  marepvfval  22509  submafval  22523  submaval  22525  mdetleib2  22532  mdet0pr  22536  m1detdiag  22541  mdetrsca  22547  mdetrsca2  22548  mdetrlin2  22551  mdetralt  22552  mdetralt2  22553  mdetunilem2  22557  mdetunilem5  22560  mdetunilem9  22564  mdetuni0  22565  m2detleib  22575  madufval  22581  symgmatr01lem  22597  symgmatr01  22598  gsummatr01lem3  22601  gsummatr01lem4  22602  gsummatr01  22603  smadiadetlem3  22612  smadiadetglem2  22616  smadiadetr  22619  mat2pmatghm  22674  cpm2mfval  22693  m2cpminvid  22697  m2cpminvid2lem  22698  m2cpminvid2  22699  decpmatval  22709  decpmataa0  22712  decpmatmul  22716  pmatcollpw1  22720  pmatcollpw2lem  22721  monmatcollpw  22723  pmatcollpwlem  22724  pmatcollpw  22725  pmatcollpwscmatlem2  22734  pm2mpval  22739  pm2mpcl  22741  pm2mpf1  22743  mptcoe1matfsupp  22746  mp2pm2mplem3  22752  mp2pm2mplem4  22753  pm2mpghm  22760  pm2mpmhmlem2  22763  chpmat1dlem  22779  chp0mat  22790  fvmptnn04ifa  22794  fvmptnn04ifb  22795  fvmptnn04ifc  22796  fvmptnn04ifd  22797  cpmadugsumlemB  22818  chcoeffeqlem  22829  epttop  22953  ordtbas2  23135  ordtopn1  23138  ordtopn2  23139  lmss  23242  2ndci  23392  2ndcsep  23403  dis2ndc  23404  1stcelcls  23405  dissnlocfin  23473  ptbasid  23519  xkoopn  23533  prdstopn  23572  ptrescn  23583  txlm  23592  lmcn2  23593  tx1stc  23594  xkopt  23599  cnmpt2c  23614  cnmptk1  23625  cnmpt1k  23626  cnmptkk  23627  qtopeu  23660  txswaphmeolem  23748  xpstopnlem1  23753  ptcmpfi  23757  xkohmeo  23759  rnelfmlem  23896  rnelfm  23897  hauspwpwf1  23931  lmflf  23949  flfcnp2  23951  alexsubb  23990  tmdgsum  24039  tgpconncomp  24057  qustgphaus  24067  tsmsfbas  24072  tsmspropd  24076  tsmssplit  24096  tsmsxplem1  24097  tsmsxplem2  24098  ustuqtop4  24188  imasdsf1olem  24317  blfvalps  24327  stdbdxmet  24459  met2ndci  24466  prdsxmslem2  24473  metustexhalf  24500  cfilucfil  24503  restmetu  24514  nmfval  24532  nmpropd  24538  nmpropd2  24539  subgnm  24577  tng0  24587  tngnm  24595  tnggrpr  24599  tngngp3  24600  tngnrg  24618  sranlm  24628  qdensere  24713  mpomulcn  24814  fsumcn  24817  cncfcompt2  24857  cncfmpt1f  24863  negfcncf  24873  oprpiece1res2  24906  htpyid  24932  phtpyid  24944  pcofval  24966  pcopt2  24979  om1bas  24987  om1plusg  24990  om1tset  24991  pi1bas  24994  pi1bas2  24997  pi1eluni  24998  pi1bas3  24999  pi1cpbl  25000  pi1addf  25003  pi1addval  25004  pi1grplem  25005  pi1xfr  25011  pi1xfrcnvlem  25012  pi1coghm  25017  cphassr  25168  tcphphl  25183  ipcau2  25190  cphipval  25199  lmnn  25219  iscau  25232  cmetcaulem  25244  iscmet3lem1  25247  causs  25254  lmclim  25259  srabn  25316  rrxprds  25345  rrxip  25346  rrxcph  25348  rrxds  25349  rrxmvallem  25360  rrxmval  25361  rrxdsfival  25369  ehl2eudisval  25379  divcncf  25404  ovollb2lem  25445  ovolfiniun  25458  ovolicc2lem4  25477  shftmbl  25495  volfiniun  25504  ioombl1lem4  25518  uniioombllem2  25540  uniioombllem6  25545  vitalilem4  25568  mbfmulc2lem  25604  mbfmulc2re  25605  mbfneg  25607  mbfaddlem  25617  mbfadd  25618  mbfsub  25619  mbfmulc2  25620  0plef  25629  0pledm  25630  itg1ge0  25643  i1faddlem  25650  i1fmullem  25651  i1fmulclem  25659  itg1mulc  25661  itg1lea  25669  itg1le  25670  mbfi1flimlem  25679  mbfmullem2  25681  mbfmul  25683  xrge0f  25688  itg2ge0  25692  itg2const  25697  itg2const2  25698  itg2uba  25700  itg2lea  25701  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  isibl2  25723  iblitg  25725  itgcl  25741  ibl0  25744  iblcnlem1  25745  itgcnlem  25747  iblss  25762  iblss2  25763  i1fibl  25765  itgitg1  25766  itgle  25767  itgeqa  25771  iblconst  25775  ibladdlem  25777  ibladd  25778  itgaddlem1  25780  itgfsum  25784  iblabslem  25785  iblabs  25786  iblabsr  25787  iblmulc2  25788  itgmulc2lem1  25789  itgsplit  25793  bddmulibl  25796  bddibl  25797  bddiblnc  25799  limccnp2  25849  limcco  25850  dvidlem  25872  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvaddf  25901  dvcmulf  25904  dvexp  25913  dvmptadd  25920  dvmptmul  25921  dvmptco  25932  dvmptfsum  25935  dvcnvlem  25936  dvef  25940  rolle  25950  mvth  25953  dvlip  25954  dvlipcn  25955  lhop1lem  25974  itgsubstlem  26011  itgpowd  26013  ply1divalg2  26100  uc1pmon1p  26113  q1pval  26116  r1pval  26119  elply2  26157  elplyr  26162  plypf1  26173  plyaddlem1  26174  coeeulem  26185  plyco  26202  coeaddlem  26210  coemulc  26216  dgradd2  26230  dgrcolem1  26235  dgrcolem2  26236  dgrco  26237  ofmulrt  26245  plydivlem3  26259  plydivlem4  26260  plyrem  26269  iaa  26289  aareccl  26290  aannenlem2  26293  aaliou3lem3  26308  aaliou3lem7  26313  taylfval  26322  taylply2  26331  taylply2OLD  26332  dvntaylp  26335  taylthlem2  26338  taylthlem2OLD  26339  ulmclm  26352  ulmres  26353  ulmshftlem  26354  ulm0  26356  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  mtest  26369  mtestbdd  26370  iblulm  26372  itgulm  26373  pserulm  26387  pserdvlem2  26394  abelthlem5  26401  abelthlem6  26402  abelthlem8  26405  abelthlem9  26406  sincn  26410  coscn  26411  efcvx  26415  efabl  26515  logfac  26566  logcn  26612  chordthmlem  26798  chordthmlem5  26802  mcubic  26813  leibpi  26908  efrlim  26935  efrlimOLD  26936  amgmlem  26956  lgamgulmlem2  26996  basellem7  27053  basellem9  27055  musum  27157  chtublem  27178  logexprlim  27192  dchrbas  27202  dchr1cl  27218  dchrabl  27221  dchrfi  27222  dchrhash  27238  bposlem6  27256  lgsdir2lem5  27296  gausslemma2dlem1  27333  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquad2lem2  27352  2lgslem1b  27359  2lgslem3b1  27368  2lgslem3c1  27369  2lgsoddprmlem4  27382  2sqlem8  27393  2sqlem11  27396  2sqreulem1  27413  2sqreunnlem1  27416  chtppilimlem2  27441  chebbnd2  27444  chpchtlim  27446  chpo1ub  27447  vmadivsum  27449  rpvmasumlem  27454  dchrisum0re  27480  dchrisum0  27487  mudivsum  27497  selberglem1  27512  selberglem2  27513  selberg2lem  27517  selberg2  27518  pntrsumo1  27532  selbergr  27535  abvcxp  27582  nosupfv  27674  noinffv  27689  madecut  27879  elons2  28254  oncutlt  28260  oniso  28267  seqsfn  28305  seqs1  28306  seqsp1  28307  n0fincut  28351  zcuts  28403  twocut  28419  expsval  28421  pw2cut2  28458  z12addscl  28473  z12shalf  28476  z12zsodd  28478  istrkgld  28531  istrkg2ld  28532  tgsegconeq  28558  tgbtwnouttr2  28567  ercgrg  28589  cgr3id  28591  tgbtwnxfr  28602  motgrp  28615  tgbtwnconn1lem3  28646  legov  28657  legid  28659  btwnleg  28660  legbtwn  28666  mirreu3  28726  mirinv  28738  miduniq1  28758  colmid  28760  krippenlem  28762  israg  28769  ragcgr  28779  motrag  28780  perpneq  28786  isperp2  28787  isperp2d  28788  footexALT  28790  footexlem1  28791  footexlem2  28792  foot  28794  perprag  28798  perpdragALT  28799  colperpexlem1  28802  mideulem2  28806  opphllem2  28820  opphllem3  28821  opphllem4  28822  midbtwn  28851  midcom  28854  mirmid  28855  lmieu  28856  lmif  28857  islmib  28859  lmilmi  28861  lmieq  28863  lmiinv  28864  lmiisolem  28868  hypcgrlem1  28871  hypcgrlem2  28872  lmiopp  28874  trgcopyeu  28878  iscgra  28881  iscgra1  28882  iscgrad  28883  sacgr  28903  isinag  28910  isinagd  28911  inagflat  28912  inaghl  28917  isleag  28919  isleagd  28920  ttgval  28947  cchhllem  28959  usgredg4  29290  ushgredgedg  29302  ushgredgedgloop  29304  usgrstrrepe  29308  uspgr1e  29317  uhgrspan1  29376  usgrres1  29388  nbgrnself  29432  nbusgredgeu  29439  cusgrfilem2  29530  finsumvtxdg2size  29624  finsumvtxdgeven  29626  wlk1walk  29712  uspgr2wlkeq  29719  uspgr2wlkeqi  29721  wlkonwlk  29734  wlkonwlk1l  29735  usgr2trlncl  29833  crctcshwlkn0lem7  29889  wwlksnredwwlkn  29968  wwlksnextbij  29975  wwlksnextprop  29985  wwlksnwwlksnon  29988  elwwlks2ons3im  30027  clwlkclwwlk2  30078  clwlkclwwlkfo  30084  clwlkclwwlkf1  30085  clwwlkwwlksb  30129  clwlknf1oclwwlkn  30159  clwwlknonmpo  30164  clwwlknonex2lem2  30183  0pthon1  30203  uhgr3cyclex  30257  iseupth  30276  eupth0  30289  eupth2lem2  30294  frgr3vlem1  30348  3vfriswmgrlem  30352  2clwwlk2clwwlklem  30421  wlkl0  30442  numclwlk1lem2  30445  grpodivfval  30609  dipfval  30777  ipval2  30782  lnoval  30827  minvecolem3  30951  h2hcau  31054  h2hlm  31055  opsqrlem3  32217  opsqrlem4  32218  foresf1o  32579  disjnf  32645  disjdifprg  32650  iundisjf  32664  br8d  32686  fnfvor  32687  ofrco  32688  ofrn2  32718  off2  32719  ofresid  32720  fmptcof2  32735  aciunf1  32741  ofpreima  32743  padct  32797  f1ocnt  32880  sgnneg  32914  prodindf  32944  indf1ofs  32948  wrdfsupp  33019  wrdpmcl  33020  pfxf1  33024  s1f1  33025  wrdt2ind  33035  swrdrn2  33036  ressnm  33046  abvpropd2  33047  ismntd  33066  dfmgc2lem  33077  pwrssmgc  33082  gsummpt2d  33132  gsummptf1od  33138  gsummptfsf1o  33143  gsumhashmul  33150  gsumwrd2dccat  33160  wrdpmtrlast  33175  psgnfzto1stlem  33182  fzto1st1  33184  tocycfv  33191  cycpmcl  33198  tocycf  33199  tocyc01  33200  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cycpm3cl2  33218  cycpmconjv  33224  tocyccntz  33226  cyc3evpm  33232  cyc3genpm  33234  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  sgnsv  33242  inftmrel  33262  isinftm  33263  submarchi  33268  isslmd  33284  urpropd  33313  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrun  33331  erlval  33340  rlocval  33341  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  rloccring  33352  resv0g  33419  resvcmn  33421  imaslmod  33434  imasmhm  33435  imasghm  33436  imasrhm  33437  imaslmhm  33438  znfermltl  33447  islinds5  33448  ellspds  33449  linds2eq  33462  lindfpropd  33463  elringlsmd  33475  nsgmgclem  33492  nsgmgc  33493  rhmquskerlem  33506  elrspunsn  33510  idlinsubrg  33512  qsidomlem1  33533  qsidomlem2  33534  opprqusbas  33569  qsdrngi  33576  rprmval  33597  rprmnz  33601  rprmnunit  33602  unitmulrprm  33609  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  1arithufdlem3  33627  dfufd2lem  33630  ply1dg1rt  33661  ply1mulrtss  33663  ply1degltlss  33677  ply1gsumz  33680  r1pquslmic  33692  mplvrpmfgalem  33709  esplyind  33731  vietalem  33735  sra1r  33737  sradrng  33738  sraidom  33739  srasubrg  33740  resssra  33743  drgext0g  33746  drgextlsp  33750  rlmdim  33766  rgmoddimOLD  33767  tnglvec  33769  tngdim  33770  matdim  33772  ply1degltdimlem  33779  lbsdiflsp0  33783  dimkerim  33784  fedgmullem2  33787  lactlmhm  33791  extdg1id  33823  ccfldsrarelvec  33828  ccfldextdgrr  33829  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspunfld  33833  fldextrspunlem2  33834  extdgfialglem1  33849  extdgfialglem2  33850  irredminply  33873  algextdeglem3  33876  algextdeglem4  33877  algextdeglem8  33881  constrsslem  33898  constrext2chnlem  33907  constrcon  33931  2sqr3nconstr  33938  cos9thpinconstrlem2  33947  1smat1  33961  submatres  33963  submateq  33966  lmatcl  33973  mdetlap1  33983  madjusmdetlem3  33986  circtopn  33994  locfinref  33998  tpr2rico  34069  lmdvglim  34111  qqhval  34129  esumeq1  34191  esumeq1d  34192  esumeq2d  34194  esumf1o  34207  esumsplit  34210  esumadd  34214  gsumesum  34216  esumlub  34217  esumaddf  34218  esumcst  34220  esumsnf  34221  esumpinfval  34230  esumcocn  34237  esummulc1  34238  esumcvg  34243  esum2d  34250  ofcval  34256  ofcfn  34257  ofcfeqd2  34258  ofcf  34260  ofcfval4  34262  ofcof  34264  sigapildsys  34319  sxval  34347  measvunilem0  34370  measvuni  34371  measiun  34375  meascnbl  34376  measinb  34378  volmeas  34388  sxbrsiga  34447  omssubadd  34457  fiunelcarsg  34473  itgeq12dv  34483  sitgval  34489  eulerpartlems  34517  eulerpartgbij  34529  eulerpartlemn  34538  sseqf  34549  sseqp1  34552  totprobd  34583  probfinmeasb  34585  probmeasb  34587  rrvadd  34609  dstfrvclim1  34635  gsumnunsn  34698  plymul02  34703  plymulx  34705  signsply0  34708  fdvneggt  34757  fdvnegge  34759  itgexpif  34763  reprpmtf1o  34783  circlemethhgt  34800  logdivsqrle  34807  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  f1resfz0f1d  35308  2cycl2d  35333  quartfull  35359  sconnpi1  35433  cvmliftphtlem  35511  cvmlift3lem2  35514  satfv1  35557  satfdmlem  35562  satf0suc  35570  satf0op  35571  sat1el2xp  35573  fmla  35575  fmlasuc0  35578  fmlafvel  35579  fmlasuc  35580  fmla1  35581  satffunlem1lem2  35597  satffunlem2lem2  35600  sategoelfvb  35613  satfv1fvfmla1  35617  2goelgoanfmla1  35618  elmsubrn  35722  msubco  35725  mthmpps  35776  r1peuqusdeg1  35837  sinccvg  35867  circum  35868  br8  35950  br4  35952  brsegle  36302  hilbert1.1  36348  itgeq2sdv  36414  ditgeq3sdv  36417  cbvoprab23davw  36470  cbvoprab13davw  36471  trer  36510  knoppcnlem4  36696  knoppcnlem9  36701  knoppcnlem11  36703  knoppndvlem6  36717  knoppf  36735  bj-imdirco  37395  bj-fvmptunsn2  37463  bj-finsumval0  37490  exrecfnlem  37584  finxpreclem1  37594  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  broucube  37855  mblfinlem2  37859  volsupnfl  37866  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  ibladdnclem  37877  itgaddnclem1  37879  itgaddnc  37881  iblabsnclem  37884  iblabsnc  37885  iblmulc2nc  37886  itgmulc2nclem1  37887  itgmulc2nclem2  37888  itgmulc2nc  37889  ftc1anclem2  37895  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  areacirc  37914  unirep  37915  upixp  37930  sdc  37945  lmclim2  37959  geomcau  37960  caures  37961  caushft  37962  prdsbnd2  37996  heibor1lem  38010  bfplem2  38024  rrncmslem  38033  isrngo  38098  iuneq2f  38357  dmec2d  38504  lflset  39319  islfld  39322  lfladdcl  39331  lflvscl  39337  lkrsc  39357  eqlkr2  39360  lshpkrlem1  39370  ldualset  39385  ldualvaddval  39391  ldualvsval  39398  ldualgrplem  39405  lduallmodlem  39412  cmtfvalN  39470  isoml  39498  iscvlat  39583  llni2  39772  lplni2  39797  lvoli3  39837  lvoli2  39841  paddfval  40057  lhpset  40255  ltrnfset  40377  trlfset  40420  cdleme21k  40598  cdlemeiota  40845  tgrpfset  41004  tgrpset  41005  tgrpabl  41011  tendo0cbv  41046  tendo02  41047  erngfset  41059  erngset  41060  erngfset-rN  41067  erngset-rN  41068  cdlemkid5  41195  cdlemkid  41196  dvafset  41264  dvaset  41265  diaffval  41290  dialss  41306  diaf11N  41309  dvhfset  41340  dvhset  41341  docaffvalN  41381  dibfval  41401  dibf11N  41421  diblss  41430  diclss  41453  dihord2cN  41481  dihord11b  41482  dihffval  41490  dihord6apre  41516  dihglblem2aN  41553  dihglblem2N  41554  dihjatcclem4  41681  lclkrs  41799  mapdh6dN  41999  mapdh6eN  42000  mapdh6fN  42001  mapdh6jN  42005  hvmapffval  42018  hvmapfval  42019  mapdh8a  42035  mapdh8ad  42039  mapdh8d0N  42042  mapdh8d  42043  mapdh8i  42046  mapdh8j  42047  mapdh9a  42049  mapdh9aOLDN  42050  hdmap1l6d  42073  hdmap1l6e  42074  hdmap1l6f  42075  hdmap1l6j  42079  hdmapval2  42092  hdmapeveclem  42094  hdmapval3lemN  42097  hdmap11lem1  42101  hgmapfval  42146  hlhils0  42205  hlhils1N  42206  hlhillvec  42211  hlhildrng  42212  hlhil0  42215  hlhillsm  42216  rhmzrhval  42225  zndvdchrrhm  42226  3factsumint1  42275  lcmineqlem12  42294  aks4d1p1p4  42325  aks4d1p1p7  42328  aks4d1p9  42342  isprimroot  42347  primrootsunit1  42351  posbezout  42354  primrootscoprbij  42356  remexz  42358  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  evl1gprodd  42371  aks6d1c2p2  42373  hashscontpow  42376  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem2  42392  aks6d1c5  42393  deg1gprod  42394  2np3bcnp1  42398  2ap1caineq  42399  sticksstones8  42407  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones17  42417  sticksstones18  42418  sticksstones19  42419  sticksstones21  42421  sticksstones22  42422  aks6d1c6lem1  42424  aks6d1c6lem2  42425  aks6d1c6lem4  42427  aks6d1c6isolem1  42428  aks5lem3a  42443  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  ofun  42492  redivcan2d  42701  redivcan3d  42702  rhmpsr1  42806  mplmapghm  42807  evlsmaprhm  42816  selvvvval  42828  evlselv  42830  selvadd  42831  selvmul  42832  fsuppind  42833  mhphf  42840  3cubeslem3r  42929  eldiophb  42999  eldioph  43000  eldioph3  43008  rabren3dioph  43057  pellqrexplicit  43119  rmxycomplete  43159  rmxynorm  43160  acongrep  43222  jm2.26a  43242  jm2.26  43244  fnwe2lem2  43293  fnwe2lem3  43294  aomclem5  43300  aomclem8  43303  imasgim  43342  isnumbasgrplem1  43343  hbtlem5  43370  dgrsub2  43377  rgspnid  43410  rngunsnply  43411  mendval  43421  mendring  43430  mendlmod  43431  mendassa  43432  nnoeomeqom  43554  tfsconcatb0  43586  oaun3  43624  safesnsupfilb  43659  fsovrfovd  44250  fsovcnvlem  44254  mnring0gd  44462  mnringlmodd  44467  mnringmulrcld  44469  colleq1  44495  colleq2  44496  dvgrat  44553  radcnvrat  44555  hashnzfzclim  44563  caofcan  44564  ofsubid  44565  ofmul12  44566  ofdivrec  44567  ofdivcan4  44568  ofdivdiv2  44569  expgrowth  44576  binomcxplemnn0  44590  binomcxplemrat  44591  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  wessf1ornlem  45429  disjf1o  45435  ssnnf1octb  45438  mapss2  45449  icof  45463  mpteq1df  45480  infnsuprnmpt  45494  upbdrech  45553  divcan8d  45560  dmmcand  45561  suplesup  45584  ssuzfz  45594  supsubc  45598  xralrple2  45599  fprodabs2  45841  fprodcn  45846  clim1fr1  45847  climrec  45849  climexp  45851  climinf  45852  climsuse  45854  climneg  45856  divcnvg  45873  sumnnodd  45876  clim2f  45880  clim2f2  45914  fnlimfvre  45918  climleltrp  45920  climreclmpt  45928  climinf2mpt  45958  climinfmpt  45959  supcnvlimsup  45984  climuzlem  45987  climisp  45990  climrescn  45992  climxrrelem  45993  climxrre  45994  liminfvalxrmpt  46030  liminflbuz2  46059  cncfcompt  46127  dvsinax  46157  fperdvper  46163  dvcosax  46170  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  iblempty  46209  iblsplit  46210  itgcoscmulx  46213  itgsincmulx  46218  itgsubsticc  46220  sublevolico  46228  stoweidlem2  46246  stoweidlem17  46261  stoweidlem21  46265  stoweidlem32  46276  stoweidlem46  46290  stoweidlem55  46299  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem3  46320  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem16  46367  fourierdlem18  46369  fourierdlem21  46372  fourierdlem22  46373  fourierdlem39  46390  fourierdlem53  46403  fourierdlem58  46408  fourierdlem59  46409  fourierdlem62  46412  fourierdlem73  46423  fourierdlem76  46426  fourierdlem81  46431  fourierdlem83  46433  fourierdlem93  46443  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fouriersw  46475  elaa2lem  46477  etransclem18  46496  etransclem32  46510  etransclem33  46511  etransclem46  46524  etransclem48  46526  rrxtopnfi  46531  rrxunitopnfi  46536  salincl  46568  sge0z  46619  sge0tsms  46624  sge0snmpt  46627  sge0sup  46635  sge0resplit  46650  sge0ss  46656  sge0isum  46671  sge0xp  46673  sge0xaddlem2  46678  sge0seq  46690  sge0reuzb  46692  meadjun  46706  meadjiun  46710  ismeannd  46711  meaiunlelem  46712  meaiininclem  46730  caragenunidm  46752  caragenuncllem  46756  omeiunltfirp  46763  carageniuncllem1  46765  caratheodorylem1  46770  0ome  46773  isomenndlem  46774  hoicvr  46792  hoicvrrex  46800  ovn0lem  46809  ovn0  46810  ovnsubaddlem1  46814  hoidmvval0  46831  hoidmvval0b  46834  hoidmv1lelem1  46835  hoidmv1le  46838  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hoidmvlelem5  46843  ovnhoilem1  46845  ovnhoilem2  46846  ovnhoi  46847  dmvon  46850  hspval  46853  ovnlecvr2  46854  hoiqssbllem2  46867  hspmbllem2  46871  hspmbl  46873  hoimbl  46875  ovnsubadd2lem  46889  ovolval4lem1  46893  ovnovollem1  46900  vonvolmbl  46905  vonvol2  46908  iccvonmbllem  46922  vonioolem2  46925  vonn0ioo2  46934  vonn0icc2  46936  smfpimltmpt  46990  issmfdmpt  46992  smfconst  46993  smfpimltxrmptf  47002  smflimlem2  47016  smflimlem3  47017  smflim  47021  smfpimgtmpt  47025  smfpimgtxrmptf  47028  smfsupmpt  47059  smfinfmpt  47063  smflimsuplem4  47067  fresfo  47294  fsetsnf  47297  fsetsnprcnex  47301  cfsetsnfsetf  47304  cfsetsnfsetfo  47306  3f1oss1  47321  f1cof1b  47323  funfocofob  47324  afveq1  47380  afveq2  47381  afvco2  47422  rspceaov  47443  faovcl  47446  afv2eq12d  47461  afv2eq1  47462  afv2eq2  47463  dfatcolem  47501  f1oresf1orab  47535  preimafvsnel  47625  preimafvelsetpreimafv  47634  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjimaid  47657  fundcmpsurinjALT  47658  ichnreuop  47718  ichreuopeq  47719  prelspr  47732  sprsymrelf1lem  47737  sprsymrelfolem2  47739  prproropreud  47755  reuopreuprim  47772  fmtnofac2lem  47814  proththd  47860  requad01  47867  dfodd6  47883  nnsum3primesprm  48036  clnbgrvtxel  48075  isgrim  48128  grimid  48132  upgrimtrls  48152  isubgrgrim  48175  clnbgrgrim  48180  usgrgrtrirex  48196  stgrnbgr0  48210  isubgr3stgrlem6  48217  isgrlim  48228  uspgrlim  48238  grlimedgclnbgr  48241  grlimgrtri  48249  grilcbri2  48257  gpgedgiov  48311  gpg5gricstgr3  48336  gpg5grlim  48339  grlimedgnedg  48377  uspgrsprfo  48394  copissgrp  48414  copisnmnd  48415  isasslaw  48438  2zrngamgm  48491  cznrng  48507  rngcvalALTV  48511  rngcbasALTV  48512  rngchomfvalALTV  48513  rngccofvalALTV  48516  rngccoALTV  48517  rngccatidALTV  48518  rhmsubcALTV  48531  ringcvalALTV  48535  ringcbasALTV  48546  ringchomfvalALTV  48547  ringccofvalALTV  48550  ringccoALTV  48551  ringccatidALTV  48552  scmsuppss  48617  ply1mulgsum  48636  dflinc2  48656  lcoop  48657  lincvalsng  48662  lincvalpr  48664  lincvalsc0  48667  lcoc0  48668  lcoel0  48674  lincsum  48675  lincolss  48680  islininds  48692  lindslinindsimp1  48703  lindsrng01  48714  snlindsntorlem  48716  lincresunit3  48727  islindeps2  48729  lmod1lem3  48735  lmod1zr  48739  itcoval  48907  itcoval0  48908  itcoval1  48909  itcoval2  48910  itcoval3  48911  itcovalsuc  48913  itcovalsucov  48914  itcovalendof  48915  itcovalpclem2  48917  itcovalt2lem2  48922  ackvalsuc1mpt  48924  ackval1  48927  ackval2  48928  ackval3  48929  ackvalsucsucval  48934  affinecomb1  48948  rrx2plordisom  48969  lines  48977  line  48978  rrxline  48980  spheres  48992  line2xlem  48999  itsclc0yqsol  49010  itscnhlinecirc02p  49031  fmpod  49115  iscnrm3llem1  49194  iscnrm3llem2  49195  iscnrm3l  49196  glbsscl  49206  posjidm  49217  posmidm  49218  toslat  49227  ipolubdm  49232  ipoglbdm  49235  mreclat  49242  topclat  49243  iinfssc  49302  iinfsubc  49303  infsubc2  49306  iinfconstbas  49311  nelsubc3  49316  initc  49336  funchomf  49342  imaidfu2lem  49354  imaidfu  49355  imaidfu2  49356  cofidf2  49365  funcoppc4  49389  fthcomf  49402  idfth  49403  idsubc  49405  upciclem1  49411  upfval2  49422  upfval3  49423  isuplem  49424  oppcup3lem  49451  uobffth  49463  uobeqw  49464  uptr2  49466  initopropd  49488  termopropd  49489  dfswapf2  49506  swapfelvv  49508  swapf1vala  49511  swapf2fn  49513  swapf2  49519  tposcurf1cl  49541  tposcurf11  49542  tposcurf12  49543  tposcurf1  49544  tposcurf2  49545  tposcurf2val  49546  tposcurf2cl  49547  tposcurfcl  49548  fucoelvv  49565  fucofvalne  49570  fuco11  49571  fuco11cl  49572  fuco21  49581  fuco11b  49582  fuco11bALT  49583  fuco22natlem3  49589  fuco22natlem  49590  fuco23a  49597  fucofunc  49604  fucofunca  49605  fucolid  49606  fucorid  49607  postcofval  49609  precofval  49612  precofvalALT  49613  precoffunc  49617  prcofelvv  49625  reldmprcof1  49626  reldmprcof2  49627  prcoftposcurfuco  49628  prcoffunc  49630  prcoffunca  49631  fucoppcco  49654  fucoppccic  49658  oppfdiag1  49659  oppfdiag1a  49660  isthincd2lem1  49670  oppcthin  49683  oppcthinco  49684  subthinc  49688  fullthinc  49695  thincciso2  49700  indthinc  49707  prsthinc  49709  setcthin  49710  setc2othin  49711  setcsnterm  49735  setc1ocofval  49739  isinito2lem  49743  dfinito4  49746  idfudiag1  49770  arweuthinc  49774  diag1f1olem  49778  prstchomval  49804  prstcprs  49805  prstcthin  49806  prstchom2  49808  oduoppcciso  49811  postcpos  49812  postcposALT  49813  postc  49814  mndtccatid  49832  mndtcid  49834  oppgoppchom  49835  oppgoppcco  49836  oppgoppcid  49837  grptcmon  49838  grptcepi  49839  2arwcat  49845  lanfval  49858  ranfval  49859  lanpropd  49860  ranpropd  49861  rellan  49868  lanrcl5  49880  ranrcl5  49885  lanup  49886  ranup  49887  lmdfval  49894  cmdfval  49895  lmdpropd  49902  cmdpropd  49903  concom  49908  coccom  49909  islmd  49910  iscmd  49911  lmddu  49912  termolmd  49915  lmdran  49916  cmdlan  49917  aacllem  50046  amgmwlem  50047