Theorem eqcomi 2830

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 2828	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 232	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1537

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

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

This theorem is referenced by:  eqtr2i  2845  eqtr3i  2846  eqtr4i  2847  syl5eqr  2870  syl5reqr  2871  syl6eqr  2874  syl6reqr  2875  eqeltrri  2910  eleqtrri  2912  eqeltrrid  2918  eleqtrrdi  2924  abeq1i  2949  abid2  2957  eqnetrri  3087  neeqtrri  3089  eqsstrri  4002  sseqtrri  4004  eqsstrrid  4016  sseqtrrdi  4018  difdif2  4261  csbprc  4358  disjssun  4417  opidg  4822  eqbrtrri  5089  breqtrri  5093  breqtrrdi  5108  opwo0id  5387  propssopi  5398  iunopeqop  5411  pwin  5454  epelg  5466  dmres  5875  xpdisj1  6018  xpdisj2  6019  resdisj  6026  cnvrescnv  6052  elid  6056  csbrn  6060  dfdm2  6132  sucprc  6266  unizlim  6307  funresfunco  6396  cnvresid  6433  fores  6600  funcoeqres  6645  f1oprg  6659  fnmptfvd  6811  fvn0ssdmfun  6842  funopdmsn  6912  fmptpr  6934  fsnunres  6950  fntpb  6972  fpropnf1  7025  soisores  7080  riotaeqimp  7140  riotaprop  7141  fnotovb  7206  orduniss2  7548  limon  7551  orduninsuc  7558  tfis  7569  fo1st  7709  fo2nd  7710  1st2val  7717  2nd2val  7718  opreuopreu  7734  el2xptp  7735  fnmpoovd  7782  cnvf1olem  7805  offsplitfpar  7815  seqomlem1  8086  om0r  8164  ixpsnf1o  8502  sbthlem5  8631  fodomr  8668  phplem4  8699  snnen2o  8707  dif1en  8751  fodomfi  8797  infssuni  8815  mapfienlem1  8868  mapfienlem2  8869  cantnf  9156  r1suc  9199  rankval4  9296  dif1card  9436  cardnum  9520  fin1a2lem13  9834  itunisuc  9841  ituniiun  9844  ttukeylem4  9934  alephval2  9994  pwfseqlem5  10085  recmulnq  10386  1lt2nq  10395  ltexnq  10397  mul02lem1  10816  addid1  10820  infrenegsup  11624  1p1e2  11763  1e2m1  11765  2p1e3  11780  3p1e4  11783  4p1e5  11784  5p1e6  11785  6p1e7  11786  7p1e8  11787  8p1e9  11788  div4p1lem1div2  11893  0mnnnnn0  11930  frnnn0supp  11954  frnnn0fsupp  11955  zeo  12069  num0u  12110  numsucc  12139  decsucc  12140  1e0p1  12141  nummac  12144  decsubi  12162  decmul10add  12168  6p5lem  12169  10m1e9  12195  5t5e25  12202  6t6e36  12207  8t6e48  12218  decbin3  12241  ige3m2fz  12932  fseq1p1m1  12982  fz0tp  13009  fz0to4untppr  13011  fzosplitpr  13147  fldiv4lem1div2uz2  13207  expneg  13438  sq4e2t8  13563  3dec  13627  faclbnd4lem1  13654  hashf  13699  hashen1  13732  pr0hash2ex  13770  hash2pr  13828  pr2pwpr  13838  hashge3el3dif  13845  hash3tr  13849  fundmge2nop0  13851  s1dm  13962  eqs1  13966  pfxccat3  14096  swrdccat  14097  pfxccatpfx2  14099  swrdccat3blem  14101  swrdccat3b  14102  repswsymballbi  14142  0csh0  14155  cats2cat  14224  s3tpop  14271  f1oun2prg  14279  s0s1  14284  s3s4  14295  s2s5  14296  s5s2  14297  wrdlen2i  14304  pfx2  14309  ccatw2s1ccatws2  14316  imi  14516  abs1m  14695  caucvg  15035  sum2id  15065  zsum  15075  hashrabrex  15180  incexclem  15191  incexc  15192  pwdif  15223  ntrivcvg  15253  prod2id  15282  fproddiv  15315  fprodfac  15327  fprodabs  15328  fproddivf  15341  fprodmodd  15351  fsumcube  15414  fprodefsum  15448  efsep  15463  3dvds  15680  3dvdsdec  15681  3dvds2dec  15682  flodddiv4  15764  lcmneg  15947  lcmf0  15978  lcmfun  15989  prmgaplem7  16393  dec2dvds  16399  1259prm  16469  2503prm  16473  4001lem1  16474  4001prm  16478  ndxid  16509  2strstr1  16605  rcaninv  17064  brcic  17068  yonedalem3b  17529  pospo  17583  oduposb  17746  oduglb  17749  odulub  17751  psssdm2  17825  letsr  17837  gsumwspan  18011  efmndbasabf  18037  submefmnd  18060  idresefmnd  18064  smndex1igid  18069  smndex1mgm  18072  smndex1sgrp  18073  smndex1mnd  18075  smndex1id  18076  smndex1n0mnd  18077  mgm2nsgrplem1  18083  mgm2nsgrplem4  18086  sgrp2nmndlem1  18088  mgmnsgrpex  18096  sgrpnmndex  18097  pwmndid  18101  mulgpropd  18269  symgbas  18499  symgplusg  18511  0symgefmndeq  18522  symgvalstruct  18525  symgtset  18527  symgsubmefmndALT  18531  pgrpsubgsymg  18537  idrespermg  18539  odlem1  18663  gexlem1  18704  sylow2a  18744  oppglsm  18767  0frgp  18905  cnaddid  18990  cnaddinv  18991  gsummptnn0fz  19106  ablfac1eu  19195  srgfcl  19265  srg1zr  19279  ring1  19352  prdsmgp  19360  pwsmgp  19368  isrhm  19473  drngui  19508  abvtrivd  19611  rmodislmod  19702  rlmval  19963  assamulgscmlem2  20129  fczpsrbag  20147  psrmulr  20164  mplcoe5lem  20248  mplcoe2  20250  opsrbaslem  20258  mpff  20317  mhpinvcl  20339  psr1val  20354  ply1plusgfvi  20410  coe1fzgsumdlem  20469  evl1fval1lem  20493  evls1var  20501  evl1gsumdlem  20519  evl1varpw  20524  cnfld0  20569  cnfld1  20570  cnfldplusf  20572  xrge0cmn  20587  gzrngunit  20611  zzngim  20699  psgninv  20726  zrhpsgnmhm  20728  zrhpsgnodpm  20736  psgndiflemB  20744  psgndiflemA  20745  dsmmval2  20880  frlmsslss  20918  islindf4  20982  mamuvs1  21014  mamuvs2  21015  mat0op  21028  matplusgcell  21042  matsubgcell  21043  matvscacell  21045  matgsum  21046  mat0dimcrng  21079  mat1dimelbas  21080  mat1dim0  21082  mat1dimscm  21084  mat1dimmul  21085  mat1f1o  21087  mat1rhmelval  21089  scmatscmiddistr  21117  smatvscl  21133  mavmuldm  21159  mdet0pr  21201  mdetdiaglem  21207  mdet0  21215  mdetralt  21217  maducoeval2  21249  madutpos  21251  cramerimplem1  21292  m2cpmmhm  21353  pmatcollpw1lem2  21383  pmatcollpwfi  21390  pmatcollpw3fi1lem1  21394  pm2mpmhm  21428  chpmatval2  21441  chpmat1d  21444  chpidmat  21455  chfacfpmmulgsum2  21473  cayleyhamilton0  21497  cayleyhamiltonALT  21499  toponrestid  21529  istpsi  21550  distopon  21605  indislem  21608  indistps2ALT  21622  distps  21623  discld  21697  restcls  21789  restntr  21790  dishaus  21990  discmp  22006  cmpsub  22008  2ndcsep  22067  dissnlocfin  22137  locfindis  22138  txbas  22175  txdis  22240  txdis1cn  22243  txkgen  22260  xkopt  22263  xkofvcn  22292  hmphdis  22404  hmphindis  22405  txhmeo  22411  txswaphmeolem  22412  xpstopnlem1  22417  ptcmpfi  22421  tmdgsum  22703  efmndtmd  22709  fmucndlem  22900  cuspcvg  22910  imasdsf1olem  22983  nrginvrcn  23301  xrsmopn  23420  zcld2  23423  ngnmcncn  23453  metnrmlem2  23468  dfii3  23491  abscncfALT  23528  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  lebnumii  23570  pcoass  23628  clmzlmvsca  23717  iscvsp  23732  cnlmod  23744  cnstrcvs  23745  cncvs  23749  isncvsngp  23753  cnindmet  23766  cnncvsmulassdemo  23768  cnncvsabsnegdemo  23769  cncmet  23925  cnflduss  23959  rrxvsca  23997  rrxplusgvscavalb  23998  ehl0  24020  ehleudis  24021  ehleudisval  24022  ehl1eudis  24023  ehl2eudis  24025  itg2cnlem2  24363  iblcnlem1  24388  itgcnlem  24390  limcdif  24474  dvmptid  24554  mvth  24589  deg1fvi  24679  dgrlt  24856  dgradd2  24858  coecj  24868  plyremlem  24893  aalioulem2  24922  sinq34lt0t  25095  efifo  25131  eff1olem  25132  circgrp  25136  circsubm  25137  loge  25170  logccv  25246  cxpsqrtlem  25285  2logb9irr  25373  2logb9irrALT  25376  sqrt2cxp2logb9e3  25377  birthday  25532  divsqrtsumlem  25557  zetacvg  25592  basellem5  25662  cht2  25749  cht3  25750  chtublem  25787  logfacbnd3  25799  logexprlim  25801  dchr1cl  25827  dchrinvcl  25829  dchrfi  25831  dchrinv  25837  dchrptlem3  25842  bclbnd  25856  bposlem6  25865  bposlem8  25867  lgsdir  25908  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3d1  25979  2lgsoddprmlem3d  25989  2sqlem9  26003  2sqlem10  26004  addsqrexnreu  26018  dchrisum0flblem1  26084  logdivsum  26109  log2sumbnd  26120  ostth2  26213  ostth  26215  lmiisolem  26582  isleagd  26634  axlowdimlem13  26740  elntg2  26771  grastruct  26815  setsvtx  26820  vtxval3sn  26828  iedgval3sn  26829  edgiedgb  26839  edg0iedg0  26840  isuhgr  26845  isushgr  26846  uhgr0  26858  isupgr  26869  isumgr  26880  umgrpredgv  26925  edglnl  26928  isuspgr  26937  isusgr  26938  ausgrusgrb  26950  usgrumgruspgr  26965  usgrf1oedg  26989  uhgr2edg  26990  usgredg3  26998  ushgredgedg  27011  ushgredgedgloop  27013  usgr0  27025  usgr1v0edg  27039  egrsubgr  27059  0grsubgr  27060  uhgrspan1  27085  upgrres  27088  umgrres  27089  usgrres  27090  upgrres1  27095  umgrres1  27096  usgrres1  27097  usgredgffibi  27106  fusgrfis  27112  dfnbgr3  27120  nbuhgr  27125  nbupgrres  27146  usgrnbcnvfv  27147  nb3grprlem2  27163  nb3gr2nb  27166  uvtxval  27169  nbupgruvtxres  27189  cplgr3v  27217  usgrexilem  27222  cusgrres  27230  cusgrsizeinds  27234  cusgrsize  27236  fusgrmaxsize  27246  vtxdgop  27252  vtxdun  27263  vtxdumgrval  27268  vdegp1bi  27319  vtxdginducedm1  27325  vtxdginducedm1fi  27326  finsumvtxdg2ssteplem1  27327  finsumvtxdg2ssteplem2  27328  finsumvtxdg2ssteplem4  27330  finsumvtxdg2size  27332  ewlksfval  27383  wlkcomp  27412  edginwlk  27416  wlk1walk  27420  uspgr2wlkeq  27427  wlkp1lem2  27456  wlkp1lem7  27461  wlkp1lem8  27462  wlkp1  27463  pthdlem1  27547  clwlkcomp  27560  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  crctcshlem4  27598  crctcshwlkn0  27599  wlkswwlksf1o  27657  wlksnwwlknvbij  27687  wwlksnwwlksnon  27694  wwlks2onv  27732  elwwlks2ons3im  27733  elwspths2spth  27746  clwlkclwwlk  27780  clwlknf1oclwwlkn  27863  clwwlknon1  27876  clwwlknon2x  27882  clwwlknonex2lem1  27886  0wlk  27895  0clwlk  27909  0clwlkv  27910  0crct  27912  0cycl  27913  wlk2v2elem2  27935  0conngr  27971  eupthp1  27995  eupth2eucrct  27996  eucrct2eupth  28024  konigsberglem1  28031  konigsberglem2  28032  konigsberglem3  28033  isfrgr  28039  frgr0  28044  frgr3v  28054  frgrncvvdeqlem3  28080  ex-dif  28202  ex-ceil  28227  ex-mod  28228  ex-gcd  28236  ex-lcm  28237  ex-ind-dvds  28240  1p1e2apr1  28245  n0lplig  28260  isgrpoi  28275  grpofo  28276  0ngrp  28288  bafval  28381  nvtri  28447  nmcnc  28473  cnbn  28646  hvsubcan2i  28841  normlem1  28887  normlem2  28888  bcseqi  28897  hhnv  28942  hhssabloilem  29038  hhshsslem1  29044  hhssvs  29049  hhsscms  29055  shscli  29094  ococi  29182  qlax1i  29404  qlaxr1i  29409  hosd1i  29599  nmcexi  29803  pjin1i  29969  hatomistici  30139  addltmulALT  30223  fresf1o  30376  padct  30455  fzodif1  30516  dp2ltsuc  30562  1mhdrd  30592  tosglb  30657  gsummptres  30690  cycpmco2lem5  30772  rhmopp  30892  fedgmullem2  31026  extdgid  31050  mdetpmtr2  31089  circtopn  31101  locfinref  31105  dispcmp  31123  tpr2uni  31148  rmulccn  31171  xrge0iifhmeo  31179  xrge0pluscn  31183  xrge0mulc1cn  31184  xrge0topn  31186  xrge0tmdALT  31189  zzsnm  31202  cnzh  31211  rezh  31212  qqh0  31225  qqh1  31226  rrhval  31237  rrhqima  31255  indsumin  31281  esumnul  31307  esum0  31308  esumpfinval  31334  esumpfinvalf  31335  esumpcvgval  31337  sitmval  31607  sitmcl  31609  eulerpartgbij  31630  eulerpartlemgf  31637  eulerpart  31640  fiblem  31656  ballotth  31795  signsw0g  31826  signstfveq0  31847  cxpcncf1  31866  itgexpif  31877  circlemethhgt  31914  hgt750lemd  31919  logdivsqrle  31921  bnj601  32192  goaleq12d  32598  satfv1  32610  satfvsucsuc  32612  satfbrsuc  32613  satf0suc  32623  satffunlem2lem2  32653  mvtval  32747  mexval  32749  mexval2  32750  mdvval  32751  mrsubcv  32757  mrsubff  32759  mrsubccat  32765  elmrsubrn  32767  elmsubrn  32775  mvhfval  32780  mpstval  32782  msrfval  32784  mstaval  32791  mthmval  32822  mthmpps  32829  problem2  32909  problem3  32910  problem4  32911  problem5  32912  quad3  32913  iprodefisumlem  32972  iprodefisum  32973  setinds  33023  bdayfo  33182  nosupbnd2lem1  33215  fobigcup  33361  unisnif  33386  fullfunfnv  33407  ivthALT  33683  ordtoplem  33783  onsucconni  33785  onsucsuccmpi  33791  limsucncmpi  33793  ordcmp  33795  dnibndlem5  33821  knoppndvlem12  33862  knoppndvlem18  33868  cnndvlem1  33876  currysetlem1  34261  bj-tagex  34302  bj-nuliota  34353  bj-nuliotaALT  34354  bj-0int  34396  bj-0nelmpt  34411  bj-inftyexpitaufo  34487  bj-elccinfty  34499  f1omptsn  34621  mptsnun  34623  istoprelowl  34644  finxp1o  34676  uncf  34886  finixpnum  34892  poimirlem16  34923  ismblfin  34948  mbfposadd  34954  dvtan  34957  itg2addnc  34961  dvasin  34993  isass  35139  ismgmOLD  35143  rngoueqz  35233  gidsn  35245  rncnv  35573  cdlemk36  38064  facp2  39115  c0exALT  39172  sqsumi  39187  nn0expgcd  39204  re0m0e0  39252  remul02  39255  prjspnval2  39287  imaiinfv  39310  eldioph2  39379  rencldnfilem  39437  elpell1qr2  39489  rmydioph  39631  kelac2  39685  islmodfg  39689  lmhmlnmsplit  39707  pwssplit4  39709  pwfi2f1o  39716  dgrsub2  39755  cytpval  39829  arearect  39842  areaquad  39843  dfrcl2  40039  relexp0eq  40066  corclrcl  40072  relexp1idm  40079  relexp0idm  40080  cotrcltrcl  40090  cortrcltrcl  40105  corclrtrcl  40106  cortrclrcl  40108  cotrclrtrcl  40109  cortrclrtrcl  40110  frege109d  40122  frege131d  40129  dfhe3  40141  fsovcnvlem  40379  clsk1independent  40416  inductionexd  40525  imo72b2lem0  40536  imo72b2lem2  40538  imo72b2  40545  unitadd  40568  amgm2d  40571  binomcxplemrat  40702  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  sbeqal2i  40752  relopabVD  41255  disjf1  41463  disjf1o  41472  fsneq  41489  fzssnn0  41605  iuneqfzuzlem  41622  uz0  41706  uzublem  41724  infxrpnf  41741  supminfxr  41760  supminfxr2  41765  iccdifioo  41811  iocopn  41816  icoopn  41821  fsumf1of  41875  fsumsermpt  41880  fprodcn  41901  lptioo2cn  41946  lptioo1cn  41947  limclner  41952  limclr  41956  climconstmpt  41959  climresmpt  41960  limsupequzmptlem  42029  liminfresicompt  42081  liminfpnfuz  42117  xlimbr  42128  fsumcncf  42181  cncfuni  42189  cncfiooicclem1  42196  cncfiooicc  42197  cxpcncf2  42203  fprodcncf  42204  fperdvper  42223  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  dvmptfprod  42250  dvnprodlem1  42251  dvnprodlem3  42253  iblempty  42270  iblsplit  42271  itgsubsticclem  42280  itgiccshift  42285  ovolsplit  42293  stoweidlem17  42322  wallispilem4  42373  wallispi2lem1  42376  wallispi2lem2  42377  stirlinglem3  42381  stirlinglem5  42383  dirkerper  42401  dirkercncflem1  42408  dirkercncflem2  42409  dirkercncflem4  42411  dirkercncf  42412  fourierdlem18  42430  fourierdlem19  42431  fourierdlem28  42440  fourierdlem30  42442  fourierdlem32  42444  fourierdlem33  42445  fourierdlem35  42447  fourierdlem36  42448  fourierdlem39  42451  fourierdlem41  42453  fourierdlem42  42454  fourierdlem46  42457  fourierdlem47  42458  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem56  42467  fourierdlem57  42468  fourierdlem60  42471  fourierdlem61  42472  fourierdlem62  42473  fourierdlem64  42475  fourierdlem65  42476  fourierdlem70  42481  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem79  42490  fourierdlem80  42491  fourierdlem90  42501  fourierdlem92  42503  fourierdlem93  42504  fourierdlem96  42507  fourierdlem97  42508  fourierdlem98  42509  fourierdlem99  42510  fourierdlem100  42511  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  etransclem35  42574  etransclem46  42585  qndenserrn  42604  ioorrnopnlem  42609  issald  42636  salgenuni  42640  salexct3  42645  salgencntex  42646  salgensscntex  42647  dmvolsal  42649  unisalgen2  42657  subsaliuncl  42661  subsalsal  42662  sge0rnn0  42670  gsumge0cl  42673  sge00  42678  sge0sn  42681  sge0tsms  42682  sge0f1o  42684  sge0prle  42703  sge0resplit  42708  sge0split  42711  sge0iunmptlemre  42717  sge0fodjrnlem  42718  sge0iun  42721  sge0isum  42729  sge0xp  42731  sge0isummpt2  42734  sge0xaddlem2  42736  sge0seq  42748  iundjiun  42762  meadjun  42764  meaunle  42766  meadjiunlem  42767  meadjiun  42768  meaiunlelem  42770  meaiuninclem  42782  meaiininclem  42788  caragenelss  42803  omeunile  42807  caragensspw  42811  caragenuncllem  42814  omelesplit  42820  carageniuncllem1  42823  carageniuncllem2  42824  caratheodorylem1  42828  caratheodory  42830  0ome  42831  hoicvr  42850  hoicvrrex  42858  ovnpnfelsup  42861  ovn02  42870  hoiprodp1  42890  hoidmv1lelem3  42895  hoidmv1le  42896  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  ovnhoilem1  42903  hoi2toco  42909  hoimbllem  42932  hoimbl  42933  ovolval2lem  42945  ovolval2  42946  ovolval3  42949  ovnsplit  42950  ovolval4lem1  42951  ovnovollem1  42958  ovnovollem2  42959  hoimbl2  42967  vonhoire  42974  vonioolem2  42983  vonicclem2  42986  vonct  42995  salpreimagelt  43006  salpreimalegt  43008  incsmf  43039  smfmbfcex  43056  decsmf  43063  smflimlem4  43070  smflim  43073  smfmullem2  43087  smfmulc1  43091  smfpimbor1lem1  43093  smfpimbor1lem2  43094  smflimsuplem2  43115  ndmaovcl  43422  ndmaovcom  43424  dfafv22  43478  rnfdmpr  43500  1t10e1p1e11  43530  fzopredsuc  43543  fmtnorec3  43730  fmtno5lem4  43738  fmtnoprmfac2lem1  43748  fmtnofac1  43752  fmtno4prmfac  43754  fmtno5fac  43764  fmtno5nprm  43765  2exp5  43775  2exp11  43785  lighneallem2  43791  lighneallem4a  43793  3exp4mod41  43801  41prothprmlem2  43803  41prothprm  43804  6even  43896  8even  43898  fppr2odd  43916  341fppr2  43919  9fppr8  43922  nfermltl2rev  43928  gbpart6  43951  gbpart8  43953  8gbe  43958  sbgoldbwt  43962  sbgoldbalt  43966  mogoldbb  43970  nnsum3primesle9  43979  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbndlem1  43990  tgblthelfgott  44000  tgoldbachlt  44001  isomushgr  44011  xpiun  44053  0mgm  44061  opmpoismgm  44094  copissgrp  44095  copisnmnd  44096  0nodd  44097  cznrnglem  44244  cznrng  44246  cznnring  44247  rngcid  44270  ringcid  44316  rhmsubclem3  44379  rhmsubclem4  44380  rhmsubcALTVlem3  44397  2t6m3t4e0  44416  zlmodzxzscm  44425  zlmodzxzadd  44426  lincvalsng  44491  lincvalsc0  44496  linc0scn0  44498  lincdifsn  44499  linc1  44500  lincsum  44504  lincscm  44505  lindslinindsimp1  44532  lindslinindimp2lem4  44536  lindslinindsimp2  44538  lmod1  44567  zlmodzxzldeplem3  44577  ldepsnlinclem1  44580  ldepsnlinclem2  44581  regt1loggt0  44616  nn0sumshdiglemB  44700  rrx2pnedifcoorneorr  44724  rrx2linest  44749  spheres  44753  itsclc0xyqsolr  44776  itsclquadb  44783