Theorem eqidd 2734

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 2733	. 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 2705

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

This theorem is referenced by:  nfabd2  2919  neleq1  3039  neleq2  3040  cbvraldvaOLD  3317  cbvrexdvaOLD  3318  rspcedeq1vd  3580  rspcedeq2vd  3581  elabd3  3622  nelrdva  3660  sbcbidv  3793  csbie2df  4392  reusngf  4626  rexreusng  4631  reuprg0  4654  iunxdif3  5045  mpteq1  5182  mpteq1i  5184  mpteq2da  5185  mpteq2dva  5186  nfcvb  5316  dfid2  5516  feq23d  6651  f10d  6802  fvmptdv2  6953  elrnrexdm  7028  f1ossf1o  7067  fmptco  7068  cofmpt  7071  fprg  7094  ftpg  7095  fmptsng  7108  fmptsnd  7109  f1dom3fv3dif  7208  f1dom3el3dif  7209  fliftfun  7252  fliftval  7256  nfriotad  7320  cbvmpo  7446  fconstmpo  7469  eqfnov2  7482  ovmpod  7504  ovmpodv2  7510  fvmpopr2d  7514  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  ovmpt3rab1  7610  elovmpt3rab  7613  ofval  7627  ofrval  7628  offn  7629  fnfvof  7633  off  7634  ofres  7635  coof  7640  ofco  7641  caofref  7647  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  caofrss  7655  caoftrn  7657  tfisi  7795  fsplitfpar  8054  fczsupp0  8129  suppssof1  8135  suppofss1d  8140  suppofss2d  8141  fvmpocurryd  8207  fpr3g  8221  iserd  8654  fsetfocdm  8791  ixpsnf1o  8868  mapxpen  9063  dffi3  9322  cantnf0  9572  cantnfp1  9578  cantnflem1  9586  ttrcltr  9613  axcclem  10355  ttukeylem3  10409  fpwwe2lem8  10536  ofsubeq0  12129  ofnegsub  12130  ofsubge0  12131  fzo0to3tp  13654  fzo1to4tp  13656  modsubmod  13838  seqid  13956  seqid2  13957  seqz  13959  seqof  13968  elovmptnn0wrd  14468  ccatdmss  14491  ccatws1ls  14543  pfxsuffeqwrdeq  14607  wrdind  14631  wrd2ind  14632  ccats1pfxeqbi  14651  repswsymb  14683  repswsymball  14688  repswsymballbi  14689  s3eq2  14779  swrds2m  14850  wrdl2exs2  14855  swrd2lsw  14861  wwlktovfo  14867  s3sndisj  14876  s3iunsndisj  14877  relexp0g  14931  relexpsucnnr  14934  relexp1g  14935  rtrclreclem1  14966  rtrclreclem4  14970  dfrtrcl2  14971  rlim2  15405  climcl  15408  rlimcl  15412  clim2  15413  rlimclim1  15454  rlimclim  15455  climrlim2  15456  climuni  15461  rlimres  15467  climeq  15476  2clim  15481  climshftlem  15483  climabs0  15494  climcn1  15501  climcn2  15502  o1of2  15522  o1rlimmul  15528  o1add2  15533  o1mul2  15534  o1sub2  15535  o1dif  15539  climsqz  15550  climsqz2  15551  rlimdiv  15555  isercoll  15577  climsup  15579  climcau  15580  caurcvgr  15583  caucvgb  15589  serf0  15590  iseralt  15594  sumz  15631  fsumss  15634  fsumsplitsn  15653  fsumsplit1  15654  fsumsplitsnun  15664  isumclim3  15668  isummulc2  15671  fsum2dlem  15679  fsumconst  15699  fsumabs  15710  fsumparts  15715  fsumrlim  15720  fsumo1  15721  seqabs  15723  cvgcmpce  15727  fsumiun  15730  ackbijnn  15737  isumshft  15748  isumltss  15757  climcndslem1  15758  climcndslem2  15759  climcnds  15760  mertenslem1  15793  mertenslem2  15794  prod1  15853  fprodss  15857  fprodconst  15887  fprod2dlem  15889  fprodsplitsn  15898  iprodclim3  15909  eftlcl  16018  reeftlcl  16019  eftlub  16020  efsep  16021  effsumlt  16022  eirrlem  16115  rpnnen2lem6  16130  rpnnen2lem7  16131  rpnnen2lem8  16132  rpnnen2lem9  16133  rpnnen2lem12  16136  2tp1odd  16265  sadasslem  16383  smupvallem  16396  smumul  16406  alginv  16488  algfx  16493  cncongr1  16580  qnumdencoprm  16658  qeqnumdivden  16659  vdwlem1  16895  vdwlem12  16906  vdwlem13  16907  prmodvdslcmf  16961  prmgap  16973  prmgaplcm  16974  prmgapprmo  16976  setsexstruct2  17088  setsstruct  17089  prdssca  17362  prdsbas  17363  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  prdsip  17367  prdsle  17368  prdsds  17370  prdstset  17372  prdshom  17373  prdsco  17374  prdsvscafval  17386  prdsdsval2  17390  prdsdsval3  17391  pwsle  17398  pwsleval  17399  pwsvscaval  17401  imasbas  17418  imasds  17419  imasplusg  17423  imasmulr  17424  imassca  17425  imasvsca  17426  imasip  17427  imastset  17428  imasle  17429  imasvscafn  17443  imasvscaval  17444  qusin  17450  xpsvsca  17483  iscat  17580  iscatd  17581  iscatd2  17589  0catg  17596  homfeq  17602  homfeqd  17603  comfffval2  17609  comffval2  17610  comfeq  17614  comfeqd  17615  oppccatid  17627  2oppccomf  17633  moni  17645  rcaninv  17703  ssc2  17731  ssctr  17734  ssceq  17735  subcssc  17749  subccat  17757  subsubc  17762  funcres  17805  funcres2  17807  idfusubc  17809  funcres2c  17812  idffth  17844  cofull  17845  cofth  17846  ressffth  17849  isnat  17859  fuccofval  17871  fuccatid  17881  fucpropd  17889  elhomai  17942  coafval  17973  setcval  17986  setcbas  17987  setchomfval  17988  setccofval  17991  setcco  17992  setccatid  17993  setcepi  17997  funcsetcres2  18002  catcval  18009  catcbas  18010  catchomfval  18011  catccofval  18013  catcco  18014  catccatid  18015  catcfuccl  18027  estrcval  18032  estrcbas  18033  estrchomfval  18034  estrccofval  18037  estrcco  18038  estrccatid  18040  estrreslem2  18046  fullestrcsetc  18059  fullsetcestrc  18074  xpcbas  18086  xpchomfval  18087  xpccofval  18090  xpccatid  18096  prfval  18107  catcxpccl  18115  xpcpropd  18116  evlfval  18125  curfval  18131  curf1  18133  curf12  18135  curf2  18137  curf2val  18138  hofval  18160  hof2fval  18163  hofcllem  18166  oppchofcl  18168  oppcyon  18177  oyoncl  18178  yonedalem4a  18183  yonedalem4b  18184  yonedainv  18189  oduposb  18235  joinval  18283  meetval  18297  isdlat  18430  ipopos  18444  pfxchn  18518  chnind  18529  chnso  18532  chnccats1  18533  chnccat  18534  chnrev  18535  gsumpropd  18588  gsumpropd2lem  18589  gsumval1  18593  gsumval2a  18595  issgrp  18630  issgrpd  18640  prdssgrpd  18643  ismndd  18666  mndprop  18670  prdsmndd  18680  imasmnd2  18684  insubm  18728  mhmima  18735  frmdbas  18762  frmdmnd  18769  efmnd  18780  smndex1gid  18813  smndex1n0mnd  18822  smndex2dlinvh  18827  sgrpnmndex  18842  resgrpplusfrn  18865  grpprop  18867  grpsubfval  18898  grpsubfvalALT  18899  grpsubpropd  18960  prdsgrpd  18965  imasgrp2  18970  imasgrp  18971  imasgrpf1  18972  mulgfval  18984  mulgfvalALT  18985  mulgnngsum  18994  mulgnn0gsum  18995  mulgpropd  19031  subgsub  19053  eqgfval  19090  qusgrp  19100  ghmqusnsglem1  19194  ghmqusnsglem2  19195  ghmqusnsg  19196  ghmquskerlem1  19197  ghmquskerlem2  19199  ghmquskerlem3  19200  ghmqusker  19201  oppgmnd  19268  oppgmndb  19269  oppggrp  19271  oppggrpb  19272  symgval  19285  symg1bas  19305  symg2bas  19307  symgvalstruct  19311  symggrp  19314  gsmsymgrfixlem1  19341  gsmsymgreqlem2  19345  symgfixels  19348  symgsssg  19381  symgfisg  19382  psgnunilem4  19411  psgnvalii  19423  oppglsm  19556  lsmelvalmi  19566  efgi0  19634  efgi1  19635  efgtf  19636  efgval2  19638  efginvrel2  19641  frgp0  19674  frgpup3lem  19691  ablprop  19707  subcmn  19751  gex2abl  19765  prdscmnd  19775  qusabl  19779  abl1  19780  cygabl  19805  gsumzf1o  19826  gsumzaddlem  19835  gsumzsplit  19841  gsumconst  19848  gsumconstf  19849  gsummptshft  19850  gsummhm2  19853  gsummptmhm  19854  gsumzunsnd  19870  gsumunsnfd  19871  gsumpt  19876  gsummptf1o  19877  gsummptun  19878  gsum2dlem2  19885  gsumcom2  19889  nn0gsumfz  19898  dprdval  19919  dprdssv  19932  dprdfeq0  19938  dprdsubg  19940  dprdspan  19943  dprdz  19946  subgdmdprd  19950  subgdprd  19951  gsumle  20059  isrng  20074  isrngd  20093  prdsrngd  20096  imasrng  20097  issrg  20108  isring  20157  ringabl  20201  ringprop  20210  isringd  20211  prdsringd  20241  prdscrngd  20242  prds1  20243  pwspjmhmmgpd  20248  imasring  20250  opprrng  20265  opprrngb  20266  opprringb  20268  dvrfval  20322  rnghmf1o  20372  c0mgm  20379  c0mhm  20380  c0snmgmhm  20382  c0snmhm  20383  rngisomring1  20388  rhmf1o  20410  pwsco1rhm  20419  pwsco2rhm  20420  zrrnghm  20453  rhmimasubrng  20483  pwsdiagrhm  20524  rngcbas  20538  rngchomfval  20539  dfrngc2  20545  rnghmsscmap2  20546  rnghmsscmap  20547  rngccat  20551  rngcid  20552  funcrngcsetc  20557  funcrngcsetcALT  20558  zrinitorngc  20559  zrtermorngc  20560  ringcbas  20567  ringchomfval  20568  dfringc2  20574  rhmsscmap2  20575  rhmsscmap  20576  ringccat  20580  ringcid  20581  rngcresringcat  20586  funcringcsetc  20591  zrtermoringc  20592  rhmsubc  20606  drngprop  20661  isdrngd  20682  isdrngrd  20683  isdrngdOLD  20684  isdrngrdOLD  20685  abvtrivd  20749  idsrngd  20773  suborng  20793  islmodd  20801  lmodabl  20844  lss1  20873  lsssn0  20883  islss3  20894  lss1d  20898  lssintcl  20899  prdslmodd  20904  idlmhm  20977  invlmhm  20978  lmhmvsca  20981  lbsextlem2  21098  sralmod  21123  sralmod0  21124  rlm0  21131  rlmvneg  21142  rnglidlmsgrp  21185  rnglidlrng  21186  qus2idrng  21212  crngridl  21219  quscrng  21222  rhmqusnsg  21224  rngqiprngimf1lem  21233  rngqiprngimf1  21239  dfcnfldOLD  21309  absabv  21363  pzriprnglem10  21429  zrhpropd  21453  fermltlchr  21468  znzrh  21481  znbas  21482  zncrng  21483  znzrhfo  21486  znf1o  21490  frgpcyg  21512  evpmodpmf1o  21535  isphld  21593  phlpropd  21594  phssip  21597  phlssphl  21598  pjfval  21645  dsmmval  21673  dsmmsubg  21682  frlmip  21717  frlmipval  21718  frlmphllem  21719  frlmphl  21720  islindf  21751  islindf4  21777  isassa  21795  isassad  21804  issubassa3  21805  sraassaOLD  21809  asclfval  21818  ressascl  21835  psrval  21854  psrbaglesupp  21861  psrbagcon  21864  psrbaglefi  21865  psrbagleadd1  21867  psrbagconf1o  21868  gsumbagdiaglem  21869  psrass1lem  21871  psrbas  21872  psrplusg  21875  psrmulr  21881  psrsca  21886  psrvscafval  21887  psrvscaval  21889  psrlmod  21898  psrlidm  21900  psrdi  21903  psrdir  21904  psrcom  21906  psrring  21908  psrassa  21911  mplsubglem  21937  mpllsslem  21938  mplvscaval  21954  mplcoe1  21973  mplcoe3  21974  mplcoe5  21976  opsrcrng  21995  opsrassa  21996  mplmon2  21997  evlslem2  22015  evlslem1  22018  mhpmulcl  22065  psdffval  22073  psdmplcl  22078  psdadd  22079  psdmul  22082  psdmvr  22085  ply1lss  22110  ply1subrg  22111  opsr0  22132  opsr1  22133  subrgply1  22146  psrplusgpropd  22149  psropprmul  22151  opsrring  22158  opsrlmod  22159  ply1mpl0  22170  ply1mpl1  22172  coe1z  22178  coe1mul2  22184  coe1tm  22188  coe1sclmulfv  22198  ply1coe  22214  evls1rhm  22238  evls1sca  22239  evl1rhm  22248  evl1sca  22250  evl1expd  22261  evl1gsumdlem  22272  evl1varpw  22277  evls1maplmhm  22293  mamufval  22308  mamudi  22319  mamudir  22320  mat0  22333  matinvg  22334  matlmod  22345  matinvgcell  22351  matring  22359  matassa  22360  mat0dimcrng  22386  mat1dim0  22389  mat1f1o  22394  dmatmulcl  22416  scmatval  22420  scmatscmiddistr  22424  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  scmatlss  22441  scmatrhmcl  22444  1mavmul  22464  mavmul0  22468  marepvfval  22481  submafval  22495  submaval  22497  mdetleib2  22504  mdet0pr  22508  m1detdiag  22513  mdetrsca  22519  mdetrsca2  22520  mdetrlin2  22523  mdetralt  22524  mdetralt2  22525  mdetunilem2  22529  mdetunilem5  22532  mdetunilem9  22536  mdetuni0  22537  m2detleib  22547  madufval  22553  symgmatr01lem  22569  symgmatr01  22570  gsummatr01lem3  22573  gsummatr01lem4  22574  gsummatr01  22575  smadiadetlem3  22584  smadiadetglem2  22588  smadiadetr  22591  mat2pmatghm  22646  cpm2mfval  22665  m2cpminvid  22669  m2cpminvid2lem  22670  m2cpminvid2  22671  decpmatval  22681  decpmataa0  22684  decpmatmul  22688  pmatcollpw1  22692  pmatcollpw2lem  22693  monmatcollpw  22695  pmatcollpwlem  22696  pmatcollpw  22697  pmatcollpwscmatlem2  22706  pm2mpval  22711  pm2mpcl  22713  pm2mpf1  22715  mptcoe1matfsupp  22718  mp2pm2mplem3  22724  mp2pm2mplem4  22725  pm2mpghm  22732  pm2mpmhmlem2  22735  chpmat1dlem  22751  chp0mat  22762  fvmptnn04ifa  22766  fvmptnn04ifb  22767  fvmptnn04ifc  22768  fvmptnn04ifd  22769  cpmadugsumlemB  22790  chcoeffeqlem  22801  epttop  22925  ordtbas2  23107  ordtopn1  23110  ordtopn2  23111  lmss  23214  2ndci  23364  2ndcsep  23375  dis2ndc  23376  1stcelcls  23377  dissnlocfin  23445  ptbasid  23491  xkoopn  23505  prdstopn  23544  ptrescn  23555  txlm  23564  lmcn2  23565  tx1stc  23566  xkopt  23571  cnmpt2c  23586  cnmptk1  23597  cnmpt1k  23598  cnmptkk  23599  qtopeu  23632  txswaphmeolem  23720  xpstopnlem1  23725  ptcmpfi  23729  xkohmeo  23731  rnelfmlem  23868  rnelfm  23869  hauspwpwf1  23903  lmflf  23921  flfcnp2  23923  alexsubb  23962  tmdgsum  24011  tgpconncomp  24029  qustgphaus  24039  tsmsfbas  24044  tsmspropd  24048  tsmssplit  24068  tsmsxplem1  24069  tsmsxplem2  24070  ustuqtop4  24160  imasdsf1olem  24289  blfvalps  24299  stdbdxmet  24431  met2ndci  24438  prdsxmslem2  24445  metustexhalf  24472  cfilucfil  24475  restmetu  24486  nmfval  24504  nmpropd  24510  nmpropd2  24511  subgnm  24549  tng0  24559  tngnm  24567  tnggrpr  24571  tngngp3  24572  tngnrg  24590  sranlm  24600  qdensere  24685  mpomulcn  24786  fsumcn  24789  cncfcompt2  24829  cncfmpt1f  24835  negfcncf  24845  oprpiece1res2  24878  htpyid  24904  phtpyid  24916  pcofval  24938  pcopt2  24951  om1bas  24959  om1plusg  24962  om1tset  24963  pi1bas  24966  pi1bas2  24969  pi1eluni  24970  pi1bas3  24971  pi1cpbl  24972  pi1addf  24975  pi1addval  24976  pi1grplem  24977  pi1xfr  24983  pi1xfrcnvlem  24984  pi1coghm  24989  cphassr  25140  tcphphl  25155  ipcau2  25162  cphipval  25171  lmnn  25191  iscau  25204  cmetcaulem  25216  iscmet3lem1  25219  causs  25226  lmclim  25231  srabn  25288  rrxprds  25317  rrxip  25318  rrxcph  25320  rrxds  25321  rrxmvallem  25332  rrxmval  25333  rrxdsfival  25341  ehl2eudisval  25351  divcncf  25376  ovollb2lem  25417  ovolfiniun  25430  ovolicc2lem4  25449  shftmbl  25467  volfiniun  25476  ioombl1lem4  25490  uniioombllem2  25512  uniioombllem6  25517  vitalilem4  25540  mbfmulc2lem  25576  mbfmulc2re  25577  mbfneg  25579  mbfaddlem  25589  mbfadd  25590  mbfsub  25591  mbfmulc2  25592  0plef  25601  0pledm  25602  itg1ge0  25615  i1faddlem  25622  i1fmullem  25623  i1fmulclem  25631  itg1mulc  25633  itg1lea  25641  itg1le  25642  mbfi1flimlem  25651  mbfmullem2  25653  mbfmul  25655  xrge0f  25660  itg2ge0  25664  itg2const  25669  itg2const2  25670  itg2uba  25672  itg2lea  25673  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itg2mono  25682  itg2i1fseqle  25683  itg2i1fseq  25684  itg2addlem  25687  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  isibl2  25695  iblitg  25697  itgcl  25713  ibl0  25716  iblcnlem1  25717  itgcnlem  25719  iblss  25734  iblss2  25735  i1fibl  25737  itgitg1  25738  itgle  25739  itgeqa  25743  iblconst  25747  ibladdlem  25749  ibladd  25750  itgaddlem1  25752  itgfsum  25756  iblabslem  25757  iblabs  25758  iblabsr  25759  iblmulc2  25760  itgmulc2lem1  25761  itgsplit  25765  bddmulibl  25768  bddibl  25769  bddiblnc  25771  limccnp2  25821  limcco  25822  dvidlem  25844  dvcnp2  25849  dvcnp2OLD  25850  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvaddf  25873  dvcmulf  25876  dvexp  25885  dvmptadd  25892  dvmptmul  25893  dvmptco  25904  dvmptfsum  25907  dvcnvlem  25908  dvef  25912  rolle  25922  mvth  25925  dvlip  25926  dvlipcn  25927  lhop1lem  25946  itgsubstlem  25983  itgpowd  25985  ply1divalg2  26072  uc1pmon1p  26085  q1pval  26088  r1pval  26091  elply2  26129  elplyr  26134  plypf1  26145  plyaddlem1  26146  coeeulem  26157  plyco  26174  coeaddlem  26182  coemulc  26188  dgradd2  26202  dgrcolem1  26207  dgrcolem2  26208  dgrco  26209  ofmulrt  26217  plydivlem3  26231  plydivlem4  26232  plyrem  26241  iaa  26261  aareccl  26262  aannenlem2  26265  aaliou3lem3  26280  aaliou3lem7  26285  taylfval  26294  taylply2  26303  taylply2OLD  26304  dvntaylp  26307  taylthlem2  26310  taylthlem2OLD  26311  ulmclm  26324  ulmres  26325  ulmshftlem  26326  ulm0  26328  ulmcau  26332  ulmss  26334  ulmbdd  26335  ulmcn  26336  mtest  26341  mtestbdd  26342  iblulm  26344  itgulm  26345  pserulm  26359  pserdvlem2  26366  abelthlem5  26373  abelthlem6  26374  abelthlem8  26377  abelthlem9  26378  sincn  26382  coscn  26383  efcvx  26387  efabl  26487  logfac  26538  logcn  26584  chordthmlem  26770  chordthmlem5  26774  mcubic  26785  leibpi  26880  efrlim  26907  efrlimOLD  26908  amgmlem  26928  lgamgulmlem2  26968  basellem7  27025  basellem9  27027  musum  27129  chtublem  27150  logexprlim  27164  dchrbas  27174  dchr1cl  27190  dchrabl  27193  dchrfi  27194  dchrhash  27210  bposlem6  27228  lgsdir2lem5  27268  gausslemma2dlem1  27305  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgsquad2lem2  27324  2lgslem1b  27331  2lgslem3b1  27340  2lgslem3c1  27341  2lgsoddprmlem4  27354  2sqlem8  27365  2sqlem11  27368  2sqreulem1  27385  2sqreunnlem1  27388  chtppilimlem2  27413  chebbnd2  27416  chpchtlim  27418  chpo1ub  27419  vmadivsum  27421  rpvmasumlem  27426  dchrisum0re  27452  dchrisum0  27459  mudivsum  27469  selberglem1  27484  selberglem2  27485  selberg2lem  27489  selberg2  27490  pntrsumo1  27504  selbergr  27507  abvcxp  27554  nosupfv  27646  noinffv  27661  madecut  27829  elons2  28196  onscutlt  28202  onsiso  28206  seqsfn  28240  seqs1  28241  seqsp1  28242  n0sfincut  28283  zscut  28332  twocut  28347  expsval  28349  pw2cut2  28383  zs12addscl  28388  zs12half  28391  zs12zodd  28393  istrkgld  28438  istrkg2ld  28439  tgsegconeq  28465  tgbtwnouttr2  28474  ercgrg  28496  cgr3id  28498  tgbtwnxfr  28509  motgrp  28522  tgbtwnconn1lem3  28553  legov  28564  legid  28566  btwnleg  28567  legbtwn  28573  mirreu3  28633  mirinv  28645  miduniq1  28665  colmid  28667  krippenlem  28669  israg  28676  ragcgr  28686  motrag  28687  perpneq  28693  isperp2  28694  isperp2d  28695  footexALT  28697  footexlem1  28698  footexlem2  28699  foot  28701  perprag  28705  perpdragALT  28706  colperpexlem1  28709  mideulem2  28713  opphllem2  28727  opphllem3  28728  opphllem4  28729  midbtwn  28758  midcom  28761  mirmid  28762  lmieu  28763  lmif  28764  islmib  28766  lmilmi  28768  lmieq  28770  lmiinv  28771  lmiisolem  28775  hypcgrlem1  28778  hypcgrlem2  28779  lmiopp  28781  trgcopyeu  28785  iscgra  28788  iscgra1  28789  iscgrad  28790  sacgr  28810  isinag  28817  isinagd  28818  inagflat  28819  inaghl  28824  isleag  28826  isleagd  28827  ttgval  28854  cchhllem  28866  usgredg4  29197  ushgredgedg  29209  ushgredgedgloop  29211  usgrstrrepe  29215  uspgr1e  29224  uhgrspan1  29283  usgrres1  29295  nbgrnself  29339  nbusgredgeu  29346  cusgrfilem2  29437  finsumvtxdg2size  29531  finsumvtxdgeven  29533  wlk1walk  29619  uspgr2wlkeq  29626  uspgr2wlkeqi  29628  wlkonwlk  29641  wlkonwlk1l  29642  usgr2trlncl  29740  crctcshwlkn0lem7  29796  wwlksnredwwlkn  29875  wwlksnextbij  29882  wwlksnextprop  29892  wwlksnwwlksnon  29895  elwwlks2ons3im  29934  clwlkclwwlk2  29985  clwlkclwwlkfo  29991  clwlkclwwlkf1  29992  clwwlkwwlksb  30036  clwlknf1oclwwlkn  30066  clwwlknonmpo  30071  clwwlknonex2lem2  30090  0pthon1  30110  uhgr3cyclex  30164  iseupth  30183  eupth0  30196  eupth2lem2  30201  frgr3vlem1  30255  3vfriswmgrlem  30259  2clwwlk2clwwlklem  30328  wlkl0  30349  numclwlk1lem2  30352  grpodivfval  30516  dipfval  30684  ipval2  30689  lnoval  30734  minvecolem3  30858  h2hcau  30961  h2hlm  30962  opsqrlem3  32124  opsqrlem4  32125  foresf1o  32486  disjnf  32552  disjdifprg  32557  iundisjf  32571  br8d  32593  fnfvor  32594  ofrco  32595  ofrn2  32624  off2  32625  ofresid  32626  fmptcof2  32641  aciunf1  32647  ofpreima  32649  padct  32705  f1ocnt  32787  sgnneg  32821  prodindf  32851  indf1ofs  32854  wrdfsupp  32925  wrdpmcl  32926  pfxf1  32930  s1f1  32931  wrdt2ind  32941  swrdrn2  32942  ressnm  32952  abvpropd2  32953  ismntd  32972  dfmgc2lem  32983  pwrssmgc  32988  gsummpt2d  33036  gsummptfsf1o  33041  gsumhashmul  33048  gsumwrd2dccat  33054  wrdpmtrlast  33069  psgnfzto1stlem  33076  fzto1st1  33078  tocycfv  33085  cycpmcl  33092  tocycf  33093  tocyc01  33094  cycpmco2f1  33100  cycpmco2rn  33101  cycpmco2lem1  33102  cycpmco2lem2  33103  cycpmco2lem3  33104  cycpmco2lem4  33105  cycpmco2lem5  33106  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmco2  33109  cycpm3cl2  33112  cycpmconjv  33118  tocyccntz  33120  cyc3evpm  33126  cyc3genpm  33128  cycpmgcl  33129  cycpmconjslem2  33131  cyc3conja  33133  sgnsv  33136  inftmrel  33156  isinftm  33157  submarchi  33162  isslmd  33178  urpropd  33206  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspn  33220  elrgspnsubrun  33223  erlval  33232  rlocval  33233  rlocbas  33241  rlocaddval  33242  rlocmulval  33243  rloccring  33244  resv0g  33310  resvcmn  33312  imaslmod  33325  imasmhm  33326  imasghm  33327  imasrhm  33328  imaslmhm  33329  znfermltl  33338  islinds5  33339  ellspds  33340  linds2eq  33353  lindfpropd  33354  elringlsmd  33366  nsgmgclem  33383  nsgmgc  33384  rhmquskerlem  33397  elrspunsn  33401  idlinsubrg  33403  qsidomlem1  33424  qsidomlem2  33425  opprqusbas  33460  qsdrngi  33467  rprmval  33488  rprmnz  33492  rprmnunit  33493  unitmulrprm  33500  1arithidomlem1  33507  1arithidomlem2  33508  1arithidom  33509  1arithufdlem3  33518  dfufd2lem  33521  ply1dg1rt  33550  ply1mulrtss  33552  ply1degltlss  33564  ply1gsumz  33566  r1pquslmic  33578  mplvrpmfgalem  33592  esplyind  33613  sra1r  33614  sradrng  33615  sraidom  33616  srasubrg  33617  resssra  33620  drgext0g  33623  drgextlsp  33627  rlmdim  33643  rgmoddimOLD  33644  tnglvec  33646  tngdim  33647  matdim  33649  ply1degltdimlem  33656  lbsdiflsp0  33660  dimkerim  33661  fedgmullem2  33664  lactlmhm  33668  extdg1id  33700  ccfldsrarelvec  33705  ccfldextdgrr  33706  fldextrspunlsplem  33707  fldextrspunlsp  33708  fldextrspunlem1  33709  fldextrspunfld  33710  fldextrspunlem2  33711  extdgfialglem1  33726  extdgfialglem2  33727  irredminply  33750  algextdeglem3  33753  algextdeglem4  33754  algextdeglem8  33758  constrsslem  33775  constrext2chnlem  33784  constrcon  33808  2sqr3nconstr  33815  cos9thpinconstrlem2  33824  1smat1  33838  submatres  33840  submateq  33843  lmatcl  33850  mdetlap1  33860  madjusmdetlem3  33863  circtopn  33871  locfinref  33875  tpr2rico  33946  lmdvglim  33988  qqhval  34006  esumeq1  34068  esumeq1d  34069  esumeq2d  34071  esumf1o  34084  esumsplit  34087  esumadd  34091  gsumesum  34093  esumlub  34094  esumaddf  34095  esumcst  34097  esumsnf  34098  esumpinfval  34107  esumcocn  34114  esummulc1  34115  esumcvg  34120  esum2d  34127  ofcval  34133  ofcfn  34134  ofcfeqd2  34135  ofcf  34137  ofcfval4  34139  ofcof  34141  sigapildsys  34196  sxval  34224  measvunilem0  34247  measvuni  34248  measiun  34252  meascnbl  34253  measinb  34255  volmeas  34265  sxbrsiga  34324  omssubadd  34334  fiunelcarsg  34350  itgeq12dv  34360  sitgval  34366  eulerpartlems  34394  eulerpartgbij  34406  eulerpartlemn  34415  sseqf  34426  sseqp1  34429  totprobd  34460  probfinmeasb  34462  probmeasb  34464  rrvadd  34486  dstfrvclim1  34512  gsumnunsn  34575  plymul02  34580  plymulx  34582  signsply0  34585  fdvneggt  34634  fdvnegge  34636  itgexpif  34640  reprpmtf1o  34660  circlemethhgt  34677  logdivsqrle  34684  hgt750lemg  34688  hgt750lemb  34690  hgt750lema  34691  f1resfz0f1d  35179  2cycl2d  35204  quartfull  35230  sconnpi1  35304  cvmliftphtlem  35382  cvmlift3lem2  35385  satfv1  35428  satfdmlem  35433  satf0suc  35441  satf0op  35442  sat1el2xp  35444  fmla  35446  fmlasuc0  35449  fmlafvel  35450  fmlasuc  35451  fmla1  35452  satffunlem1lem2  35468  satffunlem2lem2  35471  sategoelfvb  35484  satfv1fvfmla1  35488  2goelgoanfmla1  35489  elmsubrn  35593  msubco  35596  mthmpps  35647  r1peuqusdeg1  35708  sinccvg  35738  circum  35739  br8  35821  br4  35823  brsegle  36173  hilbert1.1  36219  itgeq2sdv  36285  ditgeq3sdv  36288  cbvoprab23davw  36341  cbvoprab13davw  36342  trer  36381  knoppcnlem4  36561  knoppcnlem9  36566  knoppcnlem11  36568  knoppndvlem6  36582  knoppf  36600  bj-imdirco  37255  bj-fvmptunsn2  37323  bj-finsumval0  37350  exrecfnlem  37444  finxpreclem1  37454  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem28  37708  poimirlem29  37709  poimirlem31  37711  broucube  37714  mblfinlem2  37718  volsupnfl  37725  itg2addnclem  37731  itg2addnclem3  37733  itg2addnc  37734  itg2gt0cn  37735  ibladdnclem  37736  itgaddnclem1  37738  itgaddnc  37740  iblabsnclem  37743  iblabsnc  37744  iblmulc2nc  37745  itgmulc2nclem1  37746  itgmulc2nclem2  37747  itgmulc2nc  37748  ftc1anclem2  37754  ftc1anclem4  37756  ftc1anclem5  37757  ftc1anclem6  37758  ftc1anclem7  37759  ftc1anclem8  37760  ftc1anc  37761  areacirc  37773  unirep  37774  upixp  37789  sdc  37804  lmclim2  37818  geomcau  37819  caures  37820  caushft  37821  prdsbnd2  37855  heibor1lem  37869  bfplem2  37883  rrncmslem  37892  isrngo  37957  iuneq2f  38216  dmec2d  38363  lflset  39178  islfld  39181  lfladdcl  39190  lflvscl  39196  lkrsc  39216  eqlkr2  39219  lshpkrlem1  39229  ldualset  39244  ldualvaddval  39250  ldualvsval  39257  ldualgrplem  39264  lduallmodlem  39271  cmtfvalN  39329  isoml  39357  iscvlat  39442  llni2  39631  lplni2  39656  lvoli3  39696  lvoli2  39700  paddfval  39916  lhpset  40114  ltrnfset  40236  trlfset  40279  cdleme21k  40457  cdlemeiota  40704  tgrpfset  40863  tgrpset  40864  tgrpabl  40870  tendo0cbv  40905  tendo02  40906  erngfset  40918  erngset  40919  erngfset-rN  40926  erngset-rN  40927  cdlemkid5  41054  cdlemkid  41055  dvafset  41123  dvaset  41124  diaffval  41149  dialss  41165  diaf11N  41168  dvhfset  41199  dvhset  41200  docaffvalN  41240  dibfval  41260  dibf11N  41280  diblss  41289  diclss  41312  dihord2cN  41340  dihord11b  41341  dihffval  41349  dihord6apre  41375  dihglblem2aN  41412  dihglblem2N  41413  dihjatcclem4  41540  lclkrs  41658  mapdh6dN  41858  mapdh6eN  41859  mapdh6fN  41860  mapdh6jN  41864  hvmapffval  41877  hvmapfval  41878  mapdh8a  41894  mapdh8ad  41898  mapdh8d0N  41901  mapdh8d  41902  mapdh8i  41905  mapdh8j  41906  mapdh9a  41908  mapdh9aOLDN  41909  hdmap1l6d  41932  hdmap1l6e  41933  hdmap1l6f  41934  hdmap1l6j  41938  hdmapval2  41951  hdmapeveclem  41953  hdmapval3lemN  41956  hdmap11lem1  41960  hgmapfval  42005  hlhils0  42064  hlhils1N  42065  hlhillvec  42070  hlhildrng  42071  hlhil0  42074  hlhillsm  42075  rhmzrhval  42084  zndvdchrrhm  42085  3factsumint1  42134  lcmineqlem12  42153  aks4d1p1p4  42184  aks4d1p1p7  42187  aks4d1p9  42201  isprimroot  42206  primrootsunit1  42210  posbezout  42213  primrootscoprbij  42215  remexz  42217  aks6d1c1p2  42222  aks6d1c1p3  42223  aks6d1c1p4  42224  aks6d1c1p5  42225  aks6d1c1p7  42226  evl1gprodd  42230  aks6d1c2p2  42232  hashscontpow  42235  aks6d1c2lem4  42240  aks6d1c2  42243  aks6d1c5lem2  42251  aks6d1c5  42252  deg1gprod  42253  2np3bcnp1  42257  2ap1caineq  42258  sticksstones8  42266  sticksstones10  42268  sticksstones12a  42270  sticksstones12  42271  sticksstones17  42276  sticksstones18  42277  sticksstones19  42278  sticksstones21  42280  sticksstones22  42281  aks6d1c6lem1  42283  aks6d1c6lem2  42284  aks6d1c6lem4  42286  aks6d1c6isolem1  42287  aks5lem3a  42302  grpods  42307  unitscyglem1  42308  unitscyglem2  42309  ofun  42354  redivcan2d  42564  redivcan3d  42565  rhmpsr1  42671  mplmapghm  42674  evlsvvval  42681  evlsmaprhm  42688  selvvvval  42703  evlselv  42705  selvadd  42706  selvmul  42707  fsuppind  42708  mhphf  42715  3cubeslem3r  42804  eldiophb  42874  eldioph  42875  eldioph3  42883  rabren3dioph  42932  pellqrexplicit  42994  rmxycomplete  43034  rmxynorm  43035  acongrep  43097  jm2.26a  43117  jm2.26  43119  fnwe2lem2  43168  fnwe2lem3  43169  aomclem5  43175  aomclem8  43178  imasgim  43217  isnumbasgrplem1  43218  hbtlem5  43245  dgrsub2  43252  rgspnid  43285  rngunsnply  43286  mendval  43296  mendring  43305  mendlmod  43306  mendassa  43307  nnoeomeqom  43429  tfsconcatb0  43461  oaun3  43499  safesnsupfilb  43535  fsovrfovd  44126  fsovcnvlem  44130  mnring0gd  44338  mnringlmodd  44343  mnringmulrcld  44345  colleq1  44371  colleq2  44372  dvgrat  44429  radcnvrat  44431  hashnzfzclim  44439  caofcan  44440  ofsubid  44441  ofmul12  44442  ofdivrec  44443  ofdivcan4  44444  ofdivdiv2  44445  expgrowth  44452  binomcxplemnn0  44466  binomcxplemrat  44467  binomcxplemdvbinom  44470  binomcxplemnotnn0  44473  wessf1ornlem  45306  disjf1o  45312  ssnnf1octb  45315  mapss2  45326  icof  45340  mpteq1df  45357  infnsuprnmpt  45371  upbdrech  45430  divcan8d  45437  dmmcand  45438  suplesup  45462  ssuzfz  45472  supsubc  45476  xralrple2  45477  fprodabs2  45719  fprodcn  45724  clim1fr1  45725  climrec  45727  climexp  45729  climinf  45730  climsuse  45732  climneg  45734  divcnvg  45751  sumnnodd  45754  clim2f  45758  clim2f2  45792  fnlimfvre  45796  climleltrp  45798  climreclmpt  45806  climinf2mpt  45836  climinfmpt  45837  supcnvlimsup  45862  climuzlem  45865  climisp  45868  climrescn  45870  climxrrelem  45871  climxrre  45872  liminfvalxrmpt  45908  liminflbuz2  45937  cncfcompt  46005  dvsinax  46035  fperdvper  46041  dvcosax  46048  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnxpaek  46064  dvnmul  46065  dvmptfprodlem  46066  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  iblempty  46087  iblsplit  46088  itgcoscmulx  46091  itgsincmulx  46096  itgsubsticc  46098  sublevolico  46106  stoweidlem2  46124  stoweidlem17  46139  stoweidlem21  46143  stoweidlem32  46154  stoweidlem46  46168  stoweidlem55  46177  wallispi  46192  wallispi2lem1  46193  wallispi2lem2  46194  wallispi2  46195  stirlinglem3  46198  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem16  46245  fourierdlem18  46247  fourierdlem21  46250  fourierdlem22  46251  fourierdlem39  46268  fourierdlem53  46281  fourierdlem58  46286  fourierdlem59  46287  fourierdlem62  46290  fourierdlem73  46301  fourierdlem76  46304  fourierdlem81  46309  fourierdlem83  46311  fourierdlem93  46321  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  fouriersw  46353  elaa2lem  46355  etransclem18  46374  etransclem32  46388  etransclem33  46389  etransclem46  46402  etransclem48  46404  rrxtopnfi  46409  rrxunitopnfi  46414  salincl  46446  sge0z  46497  sge0tsms  46502  sge0snmpt  46505  sge0sup  46513  sge0resplit  46528  sge0ss  46534  sge0isum  46549  sge0xp  46551  sge0xaddlem2  46556  sge0seq  46568  sge0reuzb  46570  meadjun  46584  meadjiun  46588  ismeannd  46589  meaiunlelem  46590  meaiininclem  46608  caragenunidm  46630  caragenuncllem  46634  omeiunltfirp  46641  carageniuncllem1  46643  caratheodorylem1  46648  0ome  46651  isomenndlem  46652  hoicvr  46670  hoicvrrex  46678  ovn0lem  46687  ovn0  46688  ovnsubaddlem1  46692  hoidmvval0  46709  hoidmvval0b  46712  hoidmv1lelem1  46713  hoidmv1le  46716  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoidmvlelem5  46721  ovnhoilem1  46723  ovnhoilem2  46724  ovnhoi  46725  dmvon  46728  hspval  46731  ovnlecvr2  46732  hoiqssbllem2  46745  hspmbllem2  46749  hspmbl  46751  hoimbl  46753  ovnsubadd2lem  46767  ovolval4lem1  46771  ovnovollem1  46778  vonvolmbl  46783  vonvol2  46786  iccvonmbllem  46800  vonioolem2  46803  vonn0ioo2  46812  vonn0icc2  46814  smfpimltmpt  46868  issmfdmpt  46870  smfconst  46871  smfpimltxrmptf  46880  smflimlem2  46894  smflimlem3  46895  smflim  46899  smfpimgtmpt  46903  smfpimgtxrmptf  46906  smfsupmpt  46937  smfinfmpt  46941  smflimsuplem4  46945  fresfo  47172  fsetsnf  47175  fsetsnprcnex  47179  cfsetsnfsetf  47182  cfsetsnfsetfo  47184  3f1oss1  47199  f1cof1b  47201  funfocofob  47202  afveq1  47258  afveq2  47259  afvco2  47300  rspceaov  47321  faovcl  47324  afv2eq12d  47339  afv2eq1  47340  afv2eq2  47341  dfatcolem  47379  f1oresf1orab  47413  preimafvsnel  47503  preimafvelsetpreimafv  47512  fundcmpsurbijinjpreimafv  47531  fundcmpsurinjimaid  47535  fundcmpsurinjALT  47536  ichnreuop  47596  ichreuopeq  47597  prelspr  47610  sprsymrelf1lem  47615  sprsymrelfolem2  47617  prproropreud  47633  reuopreuprim  47650  fmtnofac2lem  47692  proththd  47738  requad01  47745  dfodd6  47761  nnsum3primesprm  47914  clnbgrvtxel  47953  isgrim  48006  grimid  48010  upgrimtrls  48030  isubgrgrim  48053  clnbgrgrim  48058  usgrgrtrirex  48074  stgrnbgr0  48088  isubgr3stgrlem6  48095  isgrlim  48106  uspgrlim  48116  grlimedgclnbgr  48119  grlimgrtri  48127  grilcbri2  48135  gpgedgiov  48189  gpg5gricstgr3  48214  gpg5grlim  48217  grlimedgnedg  48255  uspgrsprfo  48272  copissgrp  48292  copisnmnd  48293  isasslaw  48316  2zrngamgm  48369  cznrng  48385  rngcvalALTV  48389  rngcbasALTV  48390  rngchomfvalALTV  48391  rngccofvalALTV  48394  rngccoALTV  48395  rngccatidALTV  48396  rhmsubcALTV  48409  ringcvalALTV  48413  ringcbasALTV  48424  ringchomfvalALTV  48425  ringccofvalALTV  48428  ringccoALTV  48429  ringccatidALTV  48430  scmsuppss  48495  ply1mulgsum  48515  dflinc2  48535  lcoop  48536  lincvalsng  48541  lincvalpr  48543  lincvalsc0  48546  lcoc0  48547  lcoel0  48553  lincsum  48554  lincolss  48559  islininds  48571  lindslinindsimp1  48582  lindsrng01  48593  snlindsntorlem  48595  lincresunit3  48606  islindeps2  48608  lmod1lem3  48614  lmod1zr  48618  itcoval  48786  itcoval0  48787  itcoval1  48788  itcoval2  48789  itcoval3  48790  itcovalsuc  48792  itcovalsucov  48793  itcovalendof  48794  itcovalpclem2  48796  itcovalt2lem2  48801  ackvalsuc1mpt  48803  ackval1  48806  ackval2  48807  ackval3  48808  ackvalsucsucval  48813  affinecomb1  48827  rrx2plordisom  48848  lines  48856  line  48857  rrxline  48859  spheres  48871  line2xlem  48878  itsclc0yqsol  48889  itscnhlinecirc02p  48910  fmpod  48994  iscnrm3llem1  49073  iscnrm3llem2  49074  iscnrm3l  49075  glbsscl  49085  posjidm  49096  posmidm  49097  toslat  49106  ipolubdm  49111  ipoglbdm  49114  mreclat  49121  topclat  49122  iinfssc  49182  iinfsubc  49183  infsubc2  49186  iinfconstbas  49191  nelsubc3  49196  initc  49216  funchomf  49222  imaidfu2lem  49234  imaidfu  49235  imaidfu2  49236  cofidf2  49245  funcoppc4  49269  fthcomf  49282  idfth  49283  idsubc  49285  upciclem1  49291  upfval2  49302  upfval3  49303  isuplem  49304  oppcup3lem  49331  uobffth  49343  uobeqw  49344  uptr2  49346  initopropd  49368  termopropd  49369  dfswapf2  49386  swapfelvv  49388  swapf1vala  49391  swapf2fn  49393  swapf2  49399  tposcurf1cl  49421  tposcurf11  49422  tposcurf12  49423  tposcurf1  49424  tposcurf2  49425  tposcurf2val  49426  tposcurf2cl  49427  tposcurfcl  49428  fucoelvv  49445  fucofvalne  49450  fuco11  49451  fuco11cl  49452  fuco21  49461  fuco11b  49462  fuco11bALT  49463  fuco22natlem3  49469  fuco22natlem  49470  fuco23a  49477  fucofunc  49484  fucofunca  49485  fucolid  49486  fucorid  49487  postcofval  49489  precofval  49492  precofvalALT  49493  precoffunc  49497  prcofelvv  49505  reldmprcof1  49506  reldmprcof2  49507  prcoftposcurfuco  49508  prcoffunc  49510  prcoffunca  49511  fucoppcco  49534  fucoppccic  49538  oppfdiag1  49539  oppfdiag1a  49540  isthincd2lem1  49550  oppcthin  49563  oppcthinco  49564  subthinc  49568  fullthinc  49575  thincciso2  49580  indthinc  49587  prsthinc  49589  setcthin  49590  setc2othin  49591  setcsnterm  49615  setc1ocofval  49619  isinito2lem  49623  dfinito4  49626  idfudiag1  49650  arweuthinc  49654  diag1f1olem  49658  prstchomval  49684  prstcprs  49685  prstcthin  49686  prstchom2  49688  oduoppcciso  49691  postcpos  49692  postcposALT  49693  postc  49694  mndtccatid  49712  mndtcid  49714  oppgoppchom  49715  oppgoppcco  49716  oppgoppcid  49717  grptcmon  49718  grptcepi  49719  2arwcat  49725  lanfval  49738  ranfval  49739  lanpropd  49740  ranpropd  49741  rellan  49748  lanrcl5  49760  ranrcl5  49765  lanup  49766  ranup  49767  lmdfval  49774  cmdfval  49775  lmdpropd  49782  cmdpropd  49783  concom  49788  coccom  49789  islmd  49790  iscmd  49791  lmddu  49792  termolmd  49795  lmdran  49796  cmdlan  49797  aacllem  49926  amgmwlem  49927