Theorem eqcomi 2815

Description: Inference from commutative law for class equality. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2813	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 221	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  eqtr2i  2829  eqtr3i  2830  eqtr4i  2831  syl5eqr  2854  syl5reqr  2855  syl6eqr  2858  syl6reqr  2859  eqeltrri  2882  eleqtrri  2884  syl5eqelr  2890  syl6eleqr  2896  abeq1i  2920  abid2  2929  eqnetrri  3049  neeqtrri  3051  eqsstr3i  3833  sseqtr4i  3835  syl5eqssr  3847  syl6sseqr  3849  difdif2  4086  csbprc  4178  disjssun  4232  opidg  4614  eqbrtrri  4867  breqtrri  4871  syl6breqr  4886  opwo0id  5150  propssopi  5163  iunopeqop  5176  pwin  5213  elid  5664  xpdisj1  5766  xpdisj2  5767  resdisj  5774  csbrn  5807  dfdm2  5881  sucprc  6013  unizlim  6057  funresfunco  6142  cnvresid  6179  fores  6340  funcoeqres  6383  f1oprg  6397  fnmptfvd  6542  fvn0ssdmfun  6572  funopdmsn  6639  fmptpr  6663  fsnunres  6679  fntpb  6698  fpropnf1  6748  soisores  6801  riotaeqimp  6858  riotaprop  6859  fnotovb  6923  orduniss2  7263  limon  7266  orduninsuc  7273  tfis  7284  fo1st  7418  fo2nd  7419  1st2val  7426  2nd2val  7427  el2xptp  7443  fnmpt2ovd  7485  fnmpt2ovdOLD  7486  cnvf1olem  7509  suppsnop  7543  seqomlem1  7781  om0r  7856  ixpsnf1o  8185  sbthlem5  8313  fodomr  8350  phplem4  8381  snnen2o  8388  dif1en  8432  fodomfi  8478  infssuni  8496  mapfienlem1  8549  mapfienlem2  8550  cantnf  8837  r1suc  8880  rankval4  8977  dif1card  9116  cardnum  9200  fin1a2lem13  9519  itunisuc  9526  ituniiun  9529  ttukeylem4  9619  alephval2  9679  recmulnq  10071  1lt2nq  10080  ltexnq  10082  mul02lem1  10497  addid1  10501  infrenegsup  11291  1p1e2  11417  1e2m1  11419  2p1e3  11434  3p1e4  11436  4p1e5  11437  5p1e6  11438  6p1e7  11439  7p1e8  11440  8p1e9  11441  div4p1lem1div2  11554  0mnnnnn0  11591  frnnn0supp  11615  frnnn0fsupp  11616  zeo  11729  num0u  11770  numsucc  11799  decsucc  11800  1e0p1  11801  nummac  11804  decsubi  11822  decmul1  11823  decmul10add  11828  6p5lem  11829  10m1e9  11855  5t5e25  11862  6t6e36  11867  8t6e48  11878  decbin3  11901  ige3m2fz  12588  fseq1p1m1  12637  fz0tp  12664  fz0to4untppr  12666  fzo0to42pr  12779  fzosplitpr  12801  fldiv4lem1div2uz2  12861  expneg  13091  sq4e2t8  13185  3dec  13273  faclbnd4lem1  13300  hashf  13345  hashen1  13378  pr0hash2ex  13413  hash2pr  13468  pr2pwpr  13478  hashge3el3dif  13485  hash3tr  13489  fundmge2nop0  13491  iswrddm0  13540  s1dm  13603  swrdccatin2  13711  swrdccatin12lem2c  13712  swrdccatin12lem3  13714  swrdccatin12  13715  swrdccat3  13716  swrdccat  13717  swrdccat3blem  13719  swrdccat3b  13720  repswsymballbi  13751  0csh0  13763  cats2cat  13831  s2dm  13859  s3tpop  13878  f1oun2prg  13886  s0s1  13891  s3s4  13902  s2s5  13903  s5s2  13904  wrdlen2i  13911  imi  14120  abs1m  14298  caucvg  14632  sum2id  14662  zsum  14672  hashrabrex  14779  incexclem  14790  incexc  14791  ntrivcvg  14850  prod2id  14879  fproddiv  14912  fprodfac  14924  fprodabs  14925  fproddivf  14938  fprodsplitf  14939  fprodge1  14946  fprodmodd  14948  fsumcube  15011  fprodefsum  15045  efsep  15060  3dvds  15275  3dvdsdec  15276  3dvds2dec  15277  flodddiv4  15356  lcmneg  15535  lcmf0  15566  lcmfun  15577  pockthi  15828  prmgaplem7  15978  dec2dvds  15984  1259prm  16054  2503prm  16058  4001lem1  16059  4001prm  16063  ndxid  16094  2strstr1  16197  homffval  16554  rcaninv  16658  brcic  16662  xpchomfval  17024  xpccofval  17027  yonedalem3b  17124  oduposb  17341  oduglb  17344  odulub  17346  psssdm2  17420  letsr  17432  gsumwspan  17588  mgm2nsgrplem1  17610  mgm2nsgrplem4  17613  sgrp2nmndlem1  17615  mgmnsgrpex  17623  sgrpnmndex  17624  mulgpropd  17786  pgrpsubgsymg  18029  idrespermg  18032  odlem1  18155  gexlem1  18195  sylow2a  18235  oppglsm  18258  0frgp  18393  cnaddid  18474  cnaddinv  18475  gsummptnn0fz  18583  gsummptnn0fzOLD  18584  ablfac1eu  18674  srgfcl  18717  srg1zr  18731  ring1  18804  prdsmgp  18812  pwsmgp  18820  isrhm  18925  drngui  18957  abvtrivd  19044  rmodislmod  19135  rlmval  19400  assamulgscmlem2  19558  fczpsrbag  19576  mplcoe5lem  19676  mplcoe2  19678  opsrbaslem  19686  mpff  19741  psr1val  19764  ply1plusgfvi  19820  coe1fzgsumdlem  19879  evl1fval1lem  19902  evls1var  19910  evl1gsumdlem  19928  evl1varpw  19933  cnfld0  19978  cnfld1  19979  cnfldplusf  19981  xrge0cmn  19996  gzrngunit  20020  zzngim  20108  psgninv  20135  zrhpsgnmhm  20137  zrhpsgnodpm  20145  psgndiflemB  20154  psgndiflemA  20155  dsmmval2  20290  frlmsslss  20323  islindf4  20387  mamuvs1  20421  mamuvs2  20422  mat0op  20435  matplusgcell  20449  matsubgcell  20450  matvscacell  20452  matgsum  20453  mat0dimcrng  20487  mat1dimelbas  20488  mat1dim0  20490  mat1dimscm  20492  mat1dimmul  20493  mat1f1o  20495  mat1rhmelval  20497  scmatscmiddistr  20525  smatvscl  20541  mavmuldm  20567  mdet0pr  20609  mdetdiaglem  20615  mdet0  20623  mdetralt  20625  maducoeval2  20657  madutpos  20659  cramerimplem1  20701  cramerimplem1OLD  20702  m2cpmmhm  20763  pmatcollpw1lem2  20793  pmatcollpwfi  20800  pmatcollpw3fi1lem1  20804  pm2mpmhm  20838  chpmatval2  20851  chpmat1d  20854  chpidmat  20865  chfacfpmmulgsum2  20883  cayleyhamilton0  20907  cayleyhamiltonALT  20909  toponrestid  20939  istpsi  20960  distopon  21015  indislem  21018  indistps2ALT  21032  distps  21033  discld  21107  restcls  21199  restntr  21200  dishaus  21400  discmp  21415  cmpsub  21417  2ndcsep  21476  dissnlocfin  21546  locfindis  21547  txbas  21584  txdis  21649  txdis1cn  21652  txkgen  21669  xkopt  21672  xkofvcn  21701  hmphdis  21813  hmphindis  21814  txhmeo  21820  txswaphmeolem  21821  xpstopnlem1  21826  ptcmpfi  21830  tmdgsum  22112  symgtgp  22118  fmucndlem  22308  cuspcvg  22318  imasdsf1olem  22391  nrginvrcn  22709  idnghm  22760  xrsmopn  22828  zcld2  22831  ngnmcncn  22861  metnrmlem2  22876  dfii3  22899  abscncfALT  22936  icopnfhmeo  22955  iccpnfhmeo  22957  xrhmeo  22958  lebnumii  22978  pcoass  23036  clmzlmvsca  23125  iscvsp  23140  cnlmod  23152  cnstrcvs  23153  cnrbas  23154  cncvs  23157  isncvsngp  23161  cnindmet  23174  cnncvsmulassdemo  23176  cnncvsabsnegdemo  23177  cncmet  23331  cnflduss  23364  itg2cnlem2  23743  iblcnlem1  23768  itgcnlem  23770  limcdif  23854  dvexp  23930  deg1fvi  24059  dgrlt  24236  dgradd2  24238  coecj  24248  plyremlem  24273  aalioulem2  24302  sinq34lt0t  24476  efifo  24508  eff1olem  24509  circgrp  24513  circsubm  24514  loge  24547  logccv  24623  cxpsqrtlem  24662  birthday  24895  divsqrtsumlem  24920  emgt0  24947  zetacvg  24955  basellem5  25025  cht2  25112  cht3  25113  chtublem  25150  logfacbnd3  25162  logexprlim  25164  dchr1cl  25190  dchrinvcl  25192  dchrfi  25194  dchrinv  25200  dchrptlem3  25205  bclbnd  25219  bposlem6  25228  bposlem8  25230  lgsdir2lem2  25265  lgsdir  25271  2lgslem3a  25335  2lgslem3b  25336  2lgslem3c  25337  2lgslem3d  25338  2lgslem3d1  25342  2lgsoddprmlem3d  25352  2sqlem9  25366  2sqlem10  25367  dchrisum0flblem1  25411  logdivsum  25436  log2sumbnd  25447  ostth2  25540  ostth  25542  lmiisolem  25902  acopyeu  25939  axlowdimlem13  26048  grastruct  26136  setsvtx  26141  vtxval3sn  26149  iedgval3sn  26150  edgiedgb  26161  edgiedgbOLD  26162  edg0iedg0  26163  edg0iedg0OLD  26164  isuhgr  26169  isushgr  26170  uhgr0  26182  isupgr  26193  isumgr  26204  umgrpredgv  26250  edglnl  26253  isuspgr  26262  isusgr  26263  ausgrusgrb  26275  usgrumgruspgr  26290  usgrf1oedg  26314  uhgr2edg  26315  usgredg3  26323  ushgredgedg  26336  ushgredgedgloop  26338  ushgredgedgloopOLD  26339  usgr0  26351  usgr1v0edg  26365  egrsubgr  26385  0grsubgr  26386  uhgrspan1  26411  upgrres  26414  umgrres  26415  usgrres  26416  upgrres1  26421  umgrres1  26422  usgrres1  26423  usgredgffibi  26432  fusgrfis  26438  dfnbgr3  26447  nbuhgr  26455  nbupgrres  26481  usgrnbcnvfv  26482  nb3grprlem2  26499  nb3gr2nb  26502  uvtxval  26505  nbupgruvtxres  26530  cplgr3v  26559  usgrexilem  26564  cusgrres  26572  cusgrsizeinds  26576  cusgrsize  26578  fusgrmaxsize  26588  vtxdgop  26594  vtxdun  26605  vtxdumgrval  26610  vdegp1bi  26661  vtxdginducedm1  26667  vtxdginducedm1fi  26668  finsumvtxdg2ssteplem1  26669  finsumvtxdg2ssteplem2  26670  finsumvtxdg2ssteplem4  26672  finsumvtxdg2size  26674  ewlksfval  26725  wlkcomp  26754  edginwlk  26758  edginwlkOLD  26759  wlk1walk  26763  uspgr2wlkeq  26770  wlkp1lem2  26799  wlkp1lem7  26804  wlkp1lem8  26805  wlkp1  26806  pthdlem1  26890  clwlkcomp  26903  crctcshwlkn0lem4  26934  crctcshwlkn0lem5  26935  crctcshwlkn0lem6  26936  crctcshlem4  26941  crctcshwlkn0  26942  wlkswwlksf1o  27006  wlknwwlksnsurOLD  27017  wlkwwlksurOLD  27025  wlksnwwlknvbij  27045  wwlksnwwlksnon  27053  wwlksnwwlksnonOLD  27055  wwlks2onv  27093  elwwlks2ons3im  27094  elwwlks2ons3OLD  27096  elwspths2spth  27109  clwlkclwwlk  27145  wwlksext2clwwlk  27207  wwlksext2clwwlkOLD  27208  clwlknf1oclwwlkn  27248  clwwlknonOLD  27256  clwwlknon1  27265  clwwlknon2x  27271  clwwlknonex2lem1  27276  0wlk  27289  0clwlk  27303  0clwlkv  27304  0crct  27306  0cycl  27307  wlk2v2elem2  27329  0conngr  27365  eupthp1  27389  eupth2eucrct  27390  eucrct2eupth  27418  konigsberglem1  27425  konigsberglem2  27426  konigsberglem3  27427  frgr0  27439  frgr3v  27450  frgrncvvdeqlem3  27476  ex-dif  27611  ex-ceil  27636  ex-mod  27637  ex-gcd  27645  ex-lcm  27646  ex-ind-dvds  27649  1p1e2apr1  27653  n0lplig  27666  isgrpoi  27681  grpofo  27682  0ngrp  27694  bafval  27787  nvtri  27853  nmcnc  27879  cnbn  28053  hvsubcan2i  28249  normlem1  28295  normlem2  28296  bcseqi  28305  hhnv  28350  hhssabloilem  28446  hhshsslem1  28452  hhssvs  28457  hhsscms  28464  shscli  28504  ococi  28592  qlax1i  28814  qlaxr1i  28819  hosd1i  29009  nmcexi  29213  pjin1i  29379  hatomistici  29549  addltmulALT  29633  fresf1o  29760  padct  29824  dp2ltsuc  29919  1mhdrd  29949  tosglb  29995  gsummptres  30109  rhmopp  30144  fzto1st1  30177  mdetpmtr2  30215  circtopn  30229  locfinref  30233  dispcmp  30251  tpr2uni  30276  rmulccn  30299  xrge0iifhmeo  30307  xrge0pluscn  30311  xrge0mulc1cn  30312  xrge0topn  30314  xrge0tmdOLD  30316  zzsnm  30330  cnzh  30339  rezh  30340  qqh0  30353  qqh1  30354  rrhval  30365  rrhqima  30383  indsumin  30409  esumnul  30435  esum0  30436  esumpfinval  30462  esumpfinvalf  30463  esumpcvgval  30465  sitmval  30736  sitmcl  30738  eulerpartgbij  30759  eulerpartlemgf  30766  eulerpart  30769  fiblem  30785  ballotth  30924  signsw0g  30958  signstfveq0  30979  cxpcncf1  30998  itgexpif  31009  circlemethhgt  31046  hgt750lemd  31051  logdivsqrle  31053  bnj601  31313  mvtval  31720  mexval  31722  mexval2  31723  mdvval  31724  mrsubcv  31730  mrsubff  31732  mrsubccat  31738  elmrsubrn  31740  elmsubrn  31748  mvhfval  31753  mpstval  31755  msrfval  31757  mstaval  31764  mthmval  31795  mthmpps  31802  problem2  31882  problem3  31883  problem4  31884  problem5  31885  quad3  31886  iprodefisumlem  31948  iprodefisum  31949  setinds  32003  bdayfo  32149  nosupbnd2lem1  32182  fobigcup  32328  unisnif  32353  fullfunfnv  32374  ivthALT  32651  ordtoplem  32751  onsucconni  32753  onsucsuccmpi  32759  limsucncmpi  32761  ordcmp  32763  dnibndlem5  32789  knoppndvlem12  32831  knoppndvlem18  32837  cnndvlem1  32845  bj-abid2  33096  bj-tagex  33285  bj-nuliota  33329  bj-nuliotaALT  33330  bj-ndxid  33341  bj-0int  33366  bj-0nelmpt  33380  bj-elccinfty  33418  f1omptsn  33501  mptsnun  33503  istoprelowl  33524  finxp1o  33545  uncf  33701  finixpnum  33707  poimirlem16  33738  ismblfin  33763  mbfposadd  33769  dvtan  33772  itg2addnc  33776  dvasin  33808  isass  33956  ismgmOLD  33960  rngoueqz  34050  gidsn  34062  rncnv  34386  cdlemk36  36694  sqsumi  37744  sqmid3api  37745  imaiinfv  37758  eldioph2  37827  rencldnfilem  37886  elpell1qr2  37938  rmydioph  38082  kelac2  38136  islmodfg  38140  lmhmlnmsplit  38158  pwssplit4  38160  pwfi2f1o  38167  dgrsub2  38206  cytpval  38288  arearect  38301  areaquad  38302  dfrcl2  38466  corclrcl  38499  relexp1idm  38506  relexp0idm  38507  cotrcltrcl  38517  cortrcltrcl  38532  corclrtrcl  38533  cortrclrcl  38535  cotrclrtrcl  38536  cortrclrtrcl  38537  frege109d  38549  frege131d  38556  dfhe3  38569  clsk1independent  38844  inductionexd  38953  imo72b2lem0  38965  imo72b2lem2  38967  imo72b2lem1  38971  imo72b2  38975  unitadd  38998  amgm2d  39001  binomcxplemrat  39049  binomcxplemdvbinom  39052  binomcxplemnotnn0  39055  sbeqal2i  39100  relopabVD  39631  disjf1  39858  founiiun0  39866  disjf1o  39867  fsneq  39885  fzssnn0  40013  iuneqfzuzlem  40030  uz0  40118  uzublem  40136  infxrpnf  40153  supminfxr  40173  supminfxr2  40178  iccdifioo  40222  iocopn  40227  icoopn  40232  fsumf1of  40286  fsumsermpt  40291  fprodcn  40312  lptioo2cn  40357  lptioo1cn  40358  limclner  40363  limclr  40367  climconstmpt  40370  climresmpt  40371  climinf2mpt  40426  climinfmpt  40427  limsupequzmptlem  40440  liminfresicompt  40492  xlimbr  40533  fsumcncf  40571  cncfuni  40579  cncfiooicclem1  40586  cncfiooicc  40587  cxpcncf2  40593  fprodcncf  40594  fperdvper  40613  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnmul  40638  dvmptfprod  40640  dvnprodlem1  40641  dvnprodlem3  40643  iblempty  40660  iblsplit  40661  itgsubsticclem  40670  itgiccshift  40675  ovolsplit  40684  stoweidlem17  40713  wallispilem4  40764  wallispi2lem1  40767  wallispi2lem2  40768  stirlinglem3  40772  stirlinglem5  40774  dirkerper  40792  dirkercncflem1  40799  dirkercncflem2  40800  dirkercncflem4  40802  dirkercncf  40803  fourierdlem18  40821  fourierdlem19  40822  fourierdlem28  40831  fourierdlem30  40833  fourierdlem32  40835  fourierdlem33  40836  fourierdlem35  40838  fourierdlem36  40839  fourierdlem39  40842  fourierdlem41  40844  fourierdlem42  40845  fourierdlem46  40848  fourierdlem47  40849  fourierdlem49  40851  fourierdlem50  40852  fourierdlem51  40853  fourierdlem56  40858  fourierdlem57  40859  fourierdlem60  40862  fourierdlem61  40863  fourierdlem62  40864  fourierdlem64  40866  fourierdlem65  40867  fourierdlem70  40872  fourierdlem73  40875  fourierdlem74  40876  fourierdlem75  40877  fourierdlem79  40881  fourierdlem80  40882  fourierdlem90  40892  fourierdlem92  40894  fourierdlem93  40895  fourierdlem96  40898  fourierdlem97  40899  fourierdlem98  40900  fourierdlem99  40901  fourierdlem100  40902  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  sqwvfoura  40924  sqwvfourb  40925  fourierswlem  40926  fouriersw  40927  etransclem35  40965  etransclem46  40976  rrxdsfi  40984  qndenserrn  40998  ioorrnopnlem  41003  issald  41030  salgenuni  41034  salexct3  41039  salgencntex  41040  salgensscntex  41041  dmvolsal  41043  unisalgen2  41051  subsaliuncl  41055  subsalsal  41056  sge0rnn0  41064  gsumge0cl  41067  sge00  41072  sge0sn  41075  sge0tsms  41076  sge0f1o  41078  sge0prle  41097  sge0resplit  41102  sge0split  41105  sge0iunmptlemre  41111  sge0fodjrnlem  41112  sge0iun  41115  sge0isum  41123  sge0xp  41125  sge0isummpt2  41128  sge0xaddlem2  41130  sge0seq  41142  iundjiun  41156  meadjun  41158  meaunle  41160  meadjiunlem  41161  meadjiun  41162  meaiunlelem  41164  meaiuninclem  41176  meaiininclem  41182  caragenelss  41197  omeunile  41201  caragensspw  41205  caragenuncllem  41208  omelesplit  41214  carageniuncllem1  41217  carageniuncllem2  41218  caratheodorylem1  41222  caratheodory  41224  0ome  41225  hoicvr  41244  hoicvrrex  41252  ovnpnfelsup  41255  ovn02  41264  hoiprodp1  41284  hoidmv1lelem3  41289  hoidmv1le  41290  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  ovnhoilem1  41297  hoi2toco  41303  hoimbllem  41326  hoimbl  41327  ovolval2lem  41339  ovolval2  41340  ovolval3  41343  ovnsplit  41344  ovolval4lem1  41345  ovnovollem1  41352  ovnovollem2  41353  hoimbl2  41361  vonhoire  41368  vonioolem2  41377  vonicclem2  41380  vonct  41389  salpreimagelt  41400  salpreimalegt  41402  incsmf  41433  smfmbfcex  41450  decsmf  41457  smflimlem4  41464  smflim  41467  smfmullem2  41481  smfmulc1  41485  smfpimbor1lem1  41487  smfpimbor1lem2  41488  smflimsuplem2  41509  ndmaovcl  41792  ndmaovcom  41794  dfafv22  41848  rnfdmpr  41871  1t10e1p1e11  41895  fzopredsuc  41908  pfx2  41987  pfxccatin12  42000  pfxccat3  42001  pfxccatpfx2  42003  fmtnorec3  42035  fmtno5lem4  42043  fmtnoprmfac2lem1  42053  fmtnofac1  42057  fmtno4prmfac  42059  fmtno5fac  42069  fmtno5nprm  42070  pwdif  42076  2exp5  42082  2exp11  42092  lighneallem2  42098  lighneallem4a  42100  3exp4mod41  42108  41prothprmlem2  42110  41prothprm  42111  6even  42195  8even  42197  gbpart6  42229  gbpart8  42231  8gbe  42236  sbgoldbwt  42240  sbgoldbalt  42244  mogoldbb  42248  nnsum3primesle9  42257  nnsum4primesodd  42259  nnsum4primesoddALTV  42260  nnsum4primeseven  42263  nnsum4primesevenALTV  42264  bgoldbtbndlem1  42268  tgblthelfgott  42278  tgoldbachlt  42279  xpiun  42334  0mgm  42342  opmpt2ismgm  42375  copissgrp  42376  copisnmnd  42377  0nodd  42378  cznrnglem  42521  cznrng  42523  cznnring  42524  rngcid  42547  ringcid  42593  rhmsubclem3  42656  rhmsubclem4  42657  rhmsubcALTVlem3  42674  2t6m3t4e0  42694  zlmodzxzscm  42703  zlmodzxzadd  42704  lincvalsng  42773  lincvalsc0  42778  linc0scn0  42780  lincdifsn  42781  linc1  42782  lincsum  42786  lincscm  42787  lindslinindsimp1  42814  lindslinindimp2lem4  42818  lindslinindsimp2  42820  lmod1  42849  zlmodzxzldeplem3  42859  ldepsnlinclem1  42862  ldepsnlinclem2  42863  regt1loggt0  42898  nn0sumshdiglemB  42982