Theorem eqeq1 2741

Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqeq1	⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2739	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  eqeq1i  2742  eqeq12OLD  2756  eqtr  2760  eqtr2  2761  iseqsetvlem  2805  eqsb1  2867  cbvexeqsetf  3495  cgsex4gOLD  3529  sbhypfOLD  3545  rexraleqim  3647  eqvincf  3650  pm13.183  3666  moeq  3713  mob  3723  euind  3730  reu2eqd  3742  reuind  3759  eqsbc1  3835  sbceqal  3851  csbhypf  3927  uniiunlem  4087  snjust  4625  elsng  4640  elprg  4648  reusngf  4674  rexreusng  4679  reuprg0  4702  rabrsn  4724  preq12bg  4853  intab  4978  uniintsn  4985  dfiun2g  5030  dfiin2g  5032  disji2  5127  disjprg  5139  unopab  5224  eusv1  5391  reusv2lem2  5399  reusv3  5405  opthg  5482  copsexgw  5495  copsexg  5496  propeqop  5512  euotd  5518  otiunsndisj  5525  elopabw  5531  solin  5619  elxpi  5707  opbrop  5783  relop  5861  ideqg  5862  dmopab2rex  5928  elrnmpt  5969  elrnmpt1  5971  elrnmptg  5972  restidsing  6071  somin1  6153  cnveqb  6216  reu3op  6312  reuop  6313  ordequn  6487  iotaval2  6529  funopg  6600  f0rn0  6793  fvelrnb  6969  fvmptg  7014  fndmin  7065  eldmrexrn  7111  foelrn  7127  foelrnf  7128  foco2  7129  fmptco  7149  funopsn  7168  funsndifnop  7171  fmptsng  7188  fmptsnd  7189  tpres  7221  eufnfv  7249  elabrex  7262  elabrexg  7263  abrexco  7264  f1veqaeq  7277  fpropnf1  7287  nf1const  7324  isosolem  7367  f1oiso  7371  eusvobj2  7423  oprabidw  7462  oprabid  7463  f1opr  7489  oprabv  7493  0mpo0  7516  elrnmpog  7568  elrnmpo  7569  elrnmpores  7571  ralrnmpo  7572  ov3  7596  ov6g  7597  ovelrn  7609  caovcang  7634  caovcan  7637  caofidlcan  7735  uniuni  7782  orduninsuc  7864  funcnvuni  7954  fiunlem  7966  fiun  7967  f1iun  7968  f1oweALT  7997  opiota  8084  eloprabi  8088  frxp  8151  funsssuppss  8215  dftpos4  8270  tz7.44-2  8447  tz7.44-3  8448  oev  8552  oalimcl  8598  omlimcl  8616  odi  8617  omeu  8623  oeeui  8640  nneob  8694  omopth  8700  eldifsucnn  8702  elqsg  8808  qsdisj  8834  qsel  8836  brecop  8850  eroveu  8852  erovlem  8853  elixpsn  8977  ixpsnf1o  8978  boxcutc  8981  2dom  9070  fundmen  9071  xpf1o  9179  nneneq  9246  nneneqOLD  9258  fofinf1o  9372  elfi  9453  elfiun  9470  dffi3  9471  brwdom  9607  brwdom3  9622  unwdomg  9624  xpwdomg  9625  noinfep  9700  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnflem1  9729  ssttrcl  9755  ttrclselem2  9766  scott0  9926  updjudhcoinrg  9973  updjud  9974  carden2a  10006  cardiun  10022  pm54.43lem  10040  alephval3  10150  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  dfac2b  10171  kmlem9  10199  kmlem12  10202  cardcf  10292  cfeq0  10296  cfsuc  10297  cff1  10298  cflim2  10303  cfss  10305  isfin5  10339  fin1a2lem11  10450  fin1a2lem13  10452  brdom7disj  10571  brdom6disj  10572  canthp1lem2  10693  canthp1  10694  tskuni  10823  gruina  10858  genpv  11039  genpelv  11040  addsrmo  11113  mulsrmo  11114  ltsosr  11134  ltresr  11180  axcnre  11204  axpre-lttri  11205  ltordlem  11788  ltord1  11789  fimaxre3  12214  supaddc  12235  supadd  12236  supmul1  12237  supmullem1  12238  supmullem2  12239  supmul  12240  creur  12260  creui  12261  nn1m1nn  12287  elz  12615  nn0ind-raph  12718  xnegeq  13249  xmullem2  13307  xmulasslem  13327  fleqceilz  13894  fseqsupubi  14019  sqeqor  14255  nn0opth2  14311  hash1snb  14458  hash2prde  14509  prprrab  14512  hash2pwpr  14515  tpf1ofv1  14536  tpf1ofv2  14537  tpfo  14539  fi1uzind  14546  wrd2ind  14761  cshfn  14828  cshf1  14848  2cshwcshw  14864  scshwfzeqfzo  14865  pfx2  14986  s3iunsndisj  15007  relexpsucnnr  15064  relexprelg  15077  rtrclreclem3  15099  shftfval  15109  sgnval  15127  01sqrexlem6  15286  reusq0  15501  summo  15753  fsum  15756  telfsumo  15838  infcvgaux1i  15893  infcvgaux2i  15894  mertenslem1  15920  mertenslem2  15921  mertens  15922  prodmo  15972  fprod  15977  ruclem12  16277  mod2eq1n2dvds  16384  divalg  16440  ndvdssub  16446  sadcp1  16492  smupp1  16517  gcdval  16533  bezoutlem1  16576  bezoutlem3  16578  bezoutlem4  16579  bezout  16580  lcmval  16629  coprmgcdb  16686  coprmdvds1  16689  divgcdcoprmex  16703  dvdsprime  16724  nprm  16725  dvdsprm  16740  coprm  16748  qnumval  16774  qdenval  16775  m1dvdsndvds  16836  reumodprminv  16842  pcval  16882  pceu  16884  pczpre  16885  pcdiv  16890  4sqlem2  16987  4sqlem4  16990  4sqlem12  16994  4sq  17002  vdwapval  17011  vdwapun  17012  vdwlem6  17024  cshwrepswhash1  17140  acsfn  17702  initoid  18046  termoid  18047  cat1lem  18141  posi  18363  gsumval2a  18698  smndex2dnrinv  18928  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2nmndlem5  18942  mgmnsgrpex  18944  sgrpnmndex  18945  cyccom  19221  ghmf1  19264  conjnmzb  19271  orbsta  19331  symgextfv  19436  symgextfo  19440  symgfixfo  19457  pmtrprfval  19505  pmtrprfvalrn  19506  psgneu  19524  psgnval  19525  psgnvali  19526  psgnvalii  19527  odfval  19550  odval  19552  dfod2  19582  submod  19587  isslw  19626  sylow2alem1  19635  sylow3lem2  19646  lsmelvalm  19669  lsmdisj2  19700  efgrelexlemb  19768  frgpup3lem  19795  cyggeninv  19901  gsumval3eu  19922  gsumval3lem2  19924  gsummpt1n0  19983  nn0gsumfz  20002  dprddisj2  20059  dpjrid  20082  pgpfac1lem3  20097  rrgeq0i  20699  domneq0  20708  domnlcanb  20720  domnrcanb  20722  abveq0  20819  abvtrivd  20833  lss1d  20961  lspsn  21000  ellspsn  21001  lspprel  21093  prmirredlem  21483  znf1o  21570  znfld  21579  znunit  21582  cygznlem3  21588  psgndif  21620  ipeq0  21656  obsip  21741  frlmphl  21801  uvcvval  21806  ellspd  21822  psrlidm  21982  psrridm  21983  psrascl  21999  mvrval2  22003  mvrf1  22006  mplmonmul  22054  evlslem3  22104  mhpsclcl  22151  psdmplcl  22166  psdmul  22170  psdmvr  22173  coe1tm  22276  coe1tmfv2  22278  cply1coe0  22305  cply1coe0bi  22306  gsummoncoe1  22312  mamufacex  22400  mat1comp  22446  mat1dimelbas  22477  mat1dimid  22480  scmatel  22511  scmateALT  22518  mavmulsolcl  22557  marrepeval  22569  marepveval  22574  mdetunilem8  22625  maducoeval2  22646  madugsum  22649  minmar1eval  22655  symgmatr01lem  22659  symgmatr01  22660  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  m2cpm  22747  m2cpminvid2lem  22760  decpmatid  22776  monmatcollpw  22785  pmatcollpw3fi1lem1  22792  mp2pm2mplem4  22815  fvmptnn04ifc  22858  chfacffsupp  22862  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  cpmadumatpoly  22889  cayleyhamilton  22896  cayleyhamiltonALT  22897  istopon  22918  toponsspwpw  22928  fctop  23011  cctop  23013  ppttop  23014  pptbas  23015  epttop  23016  t0sep  23332  t1sep2  23377  cmpsublem  23407  cmpsub  23408  unisngl  23535  txuni2  23573  elpt  23580  ptbasfi  23589  xkoopn  23597  ptpjopn  23620  ptclsg  23623  dfac14lem  23625  ptcnp  23630  ptrescn  23647  tx1stc  23658  qtopeu  23724  kqt0lem  23744  isr0  23745  hauspwpwf1  23995  xmeteq0  24348  imasf1oxmet  24385  comet  24526  stdbdxmet  24528  met2ndci  24535  prdsxmslem2  24542  nrmmetd  24587  tngngp  24675  tngngp3  24677  xrsxmet  24831  iccpnfcnv  24975  iccpnfhmeo  24976  cnheibor  24987  elovolm  25510  ovolgelb  25515  ovolicc1  25551  ovolicc  25558  ioorval  25609  uniioombllem6  25623  dyadmax  25633  dyadmbl  25635  i1fadd  25730  i1fmul  25731  itg1addlem3  25733  i1fmulc  25738  itg2l  25764  itg2leub  25769  limcmpt  25918  limcco  25928  dvcobr  25983  dvcobrOLD  25984  deg1ldg  26131  ig1pval  26215  elply  26234  elply2  26235  coeval  26262  coe1termlem  26297  coe1term  26298  quotval  26334  plydivlem4  26338  plydivex  26339  vieta1  26354  aannenlem2  26371  aalioulem2  26375  abelthlem9  26484  logtayllem  26701  logtayl  26702  isosctrlem2  26862  leibpilem2  26984  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  mpodvdsmulf1o  27237  dvdsmulf1o  27239  perfectlem2  27274  lgsfval  27346  lgsval2lem  27351  lgsqrmodndvds  27397  lgsdchrval  27398  gausslemma2dlem0i  27408  2lgslem1b  27436  2lgslem3  27448  2sqlem2  27462  2sqlem8  27470  2sqlem9  27471  2sqlem11  27473  addsq2reu  27484  dchrisum0flblem1  27552  padicval  27661  padicabv  27674  ostth1  27677  sltval2  27701  sltintdifex  27706  sltres  27707  nolt02o  27740  madef  27895  addsval2  27996  addsproplem2  28003  addsproplem4  28005  addsproplem5  28006  addsproplem6  28007  addsprop  28009  addscut  28011  sleadd1  28022  addsuniflem  28034  addsunif  28035  addsasslem1  28036  addsasslem2  28037  addsbdaylem  28049  negsprop  28067  negsid  28073  mulsval2lem  28136  mulsproplem9  28150  mulsproplem12  28153  mulsprop  28156  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  mulsunif2  28196  precsexlemcbv  28230  precsexlem9  28239  precsexlem11  28241  n0s0suc  28345  n0s0m1  28359  n0seo  28405  zseo  28406  expsval  28408  elzs12  28421  recut  28428  0reno  28429  renegscl  28430  readdscl  28431  remulscllem1  28432  remulscl  28434  axtgcgrid  28471  axtgbtwnid  28474  islmib  28795  inaghl  28853  axpaschlem  28955  axlowdimlem15  28971  axlowdim  28976  upgredg2vtx  29158  edglnl  29160  umgredgnlp  29164  usgredg2vtxeuALT  29239  uspgredg2v  29241  ushgredgedgloop  29248  nbusgredgeu  29383  cusgrfilem2  29474  cusgrfi  29476  vtxdushgrfvedg  29508  1loopgrvd2  29521  rusgr1vtxlem  29605  wlkeq  29652  wlkp1lem8  29698  upgrwlkdvdelem  29756  crctcshwlkn0lem6  29835  wlknwwlksnbij  29908  rusgrnumwwlkl1  29988  clwlkclwwlklem2a1  30011  clwwlknscsh  30081  eleclclwwlkn  30095  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknon1sn  30119  frgr3vlem1  30292  3vfriswmgrlem  30296  frgrncvvdeqlem3  30320  wlkl0  30386  frgrreggt1  30412  nvz  30688  nmosetn0  30784  nmoolb  30790  nmoubi  30791  nmlno0lem  30812  nmlno0i  30813  hvsubeq0  31087  hvaddcan  31089  normsub0  31155  norm1exi  31269  pjhval  31416  omlsii  31422  omlsi  31423  pjoml  31455  h1de2ci  31575  spansneleq  31589  h1datomi  31600  h1datom  31601  spansncv  31672  5oalem6  31678  pj11  31733  nmopsetn0  31884  nmfnsetn0  31897  nmoplb  31926  nmopub  31927  nmfnlb  31943  nmfnleub  31944  nmlnop0iALT  32014  nmlnop0  32017  lnopeq  32028  nmopun  32033  nmcexi  32045  branmfn  32124  pjnmopi  32167  pj3i  32227  atss  32365  atom1d  32372  chirred  32414  cdj3lem2  32454  eqelbid  32494  elabreximd  32529  disjxpin  32601  disjunsn  32607  br8d  32622  fmptcof2  32667  psgnfzto1stlem  33120  sgnsval  33181  elrgspnlem2  33247  elrgspnlem3  33248  domnlcanOLD  33283  linds2eq  33409  elrspunsn  33457  mxidlmax  33493  1arithidomlem1  33563  1arithidom  33565  1arithufdlem1  33572  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  1arithufd  33576  dfufd2  33578  ply1dg1rt  33604  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  rtelextdg2lem  33767  constrsuc  33779  2sqr3minply  33791  madjusmdetlem2  33827  madjusmdet  33830  zarclssn  33872  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iifhom  33936  xrge0tmd  33944  xrge0tmdALT  33945  esumc  34052  sgn3da  34544  sgnmul  34545  sgnnbi  34548  sgnpbi  34549  sgn0bi  34550  plymulx0  34562  signspval  34567  tgoldbachgt  34678  bnj1468  34860  f1resfz0f1d  35119  acycgrcycl  35152  sconnpi1  35244  cvmlift3lem2  35325  satfv0  35363  satfv1  35368  satfbrsuc  35371  satfrnmapom  35375  satfv0fun  35376  satf0op  35382  sat1el2xp  35384  fmlafvel  35390  fmla1  35392  isfmlasuc  35393  fmlaomn0  35395  gonan0  35397  goaln0  35398  gonar  35400  goalr  35402  fmla0disjsuc  35403  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem2lem1  35409  dmopab3rexdif  35410  satfv0fvfmla0  35418  sategoelfvb  35424  ex-sategoelel  35426  satfv1fvfmla1  35428  2goelgoanfmla1  35429  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  prv1n  35436  ellcsrspsn  35646  r1peuqusdeg1  35648  br8  35756  br6  35757  br4  35758  rdgprc0  35794  dfrdg2  35796  dfbigcup2  35900  elsingles  35919  dfiota3  35924  brimageg  35928  brdomaing  35936  brrangeg  35937  dfrdg4  35952  elaltxp  35976  funtransport  36032  fvtransport  36033  brsegle  36109  funray  36141  fvray  36142  funline  36143  fvline  36145  ellines  36153  linethru  36154  rankeq1o  36172  subtr  36315  subtr2  36316  nn0prpw  36324  bj-elabd2ALT  36926  bj-gabss  36936  bj-imafv  37252  topdifinffinlem  37348  topdifinffin  37349  topdifinfeq  37351  finxpreclem2  37391  finxpreclem3  37394  fvineqsnf1  37411  fvineqsneu  37412  wl-ax12v2cl  37507  wl-issetft  37583  fin2so  37614  ptrest  37626  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  poimirlem32  37659  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  ftc1anc  37708  unirep  37721  sdclem2  37749  sdclem1  37750  sdc  37751  fdc  37752  isbnd  37787  heibor1lem  37816  heiborlem4  37821  heiborlem6  37823  heiborlem10  37827  ismgmOLD  37857  maxidlmax  38050  prnc  38074  isfldidl  38075  dmnnzd  38082  disjressuc2  38389  qsdisjALTV  38616  eqvrelqsel  38617  riotasvd  38957  lshpdisj  38988  lsat0cv  39034  lcvexchlem4  39038  lcvexchlem5  39039  lshpkrlem1  39111  lshpkrlem2  39112  lshpkrlem3  39113  lshpkrcl  39117  islshpkrN  39121  atnle  39318  glbconxN  39380  isline  39741  ispointN  39744  pmapglbx  39771  ispsubcl2N  39949  lhp2atnle  40035  cdleme43fsv1snlem  40422  cdleme40v  40471  cdlemkid5  40937  cdlemkid  40938  dvhb1dimN  40988  dib1dim  41167  dicopelval  41179  dicelval1sta  41189  diclspsn  41196  dihvalcqpre  41237  dihglblem2aN  41295  dihglblem2N  41296  dih1dimatlem  41331  dihpN  41338  dochfl1  41478  lcfl7N  41503  lcf1o  41553  hvmapvalvalN  41763  hdmapval2lem  41833  aks6d1c1  42117  aks6d1c4  42125  sticksstones10  42156  sticksstones12a  42158  aks6d1c7  42185  metakunt3  42208  metakunt4  42209  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt24  42229  sn-iotalem  42260  f1o2d2  42274  fiabv  42546  evlsbagval  42576  selvvvval  42595  fsuppind  42600  absnw  42688  elrfi  42705  nacsfg  42716  mzpcompact2lem  42762  eldioph2b  42774  eldioph3  42777  eldiophss  42785  diophrex  42786  elnn0rabdioph  42814  rencldnfilem  42831  elpell1qr  42858  elpell14qr  42860  elpell1234qr  42862  jm2.27  43020  rmydioph  43026  expdiophlem2  43034  wepwsolem  43054  aomclem6  43071  lnr2i  43128  lpirlnr  43129  hbtlem2  43136  hbtlem4  43138  hbtlem5  43140  rngunsnply  43181  flcidc  43182  onsucelab  43276  limnsuc  43278  nnoeomeqom  43325  cantnfresb  43337  tfsconcatfv2  43353  tfsconcatb0  43357  oaun3lem1  43387  oadif1lem  43392  oadif1  43393  clcnvlem  43636  brtrclfv2  43740  frege55lem1c  43929  frege104  43980  clsk1indlem0  44054  clsk1indlem2  44055  clsk1indlem3  44056  clsk1indlem4  44057  clsk1indlem1  44058  pm13.192  44429  equncomVD  44888  csbingVD  44904  csbsngVD  44913  csbfv12gALTVD  44919  relopabVD  44921  refsum2cnlem1  45042  elrnmptf  45186  upbdrech  45317  ssfiunibd  45321  iccshift  45531  iooshift  45535  fsumf1of  45589  limcperiod  45643  climinf2mpt  45729  climinfmpt  45730  cncfshiftioo  45907  itgiccshift  45995  itgperiod  45996  stoweidlem46  46061  fourierdlem29  46151  fourierdlem37  46159  fourierdlem48  46169  fourierdlem51  46172  fourierdlem54  46175  fourierdlem62  46183  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem92  46213  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem103  46224  fourierdlem104  46225  fourierdlem105  46226  fourierdlem108  46229  fourierdlem110  46231  fourierdlem112  46233  etransclem1  46250  etransclem5  46254  etransclem17  46266  etransclem32  46281  etransclem41  46290  sge0f1o  46397  sge0resplit  46421  sge0fodjrnlem  46431  nnfoctbdjlem  46470  nnfoctbdj  46471  ovnval  46556  ovnlecvr  46573  ovnpnfelsup  46574  ovn0lem  46580  hoidmvval  46592  hoidmvlelem1  46610  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  hoidifhspval3  46634  hspmbllem2  46642  hoimbl  46646  ovnsubadd2  46661  ovolval5lem2  46668  ovolval5lem3  46669  ovolval5  46670  ovnovol  46674  fsetsnf  47063  fsetsnfo  47065  fcoresf1  47081  aiotaval  47107  euoreqb  47121  afv0fv0  47161  afvfv0bi  47164  afvelrnb  47175  afvelrnb0  47176  afv20defat  47244  otiunsndisjX  47291  fun2dmnopgexmpl  47296  2ffzoeq  47339  elsetpreimafvb  47371  imasetpreimafvbijlemfo  47392  fargshiftf1  47428  fargshiftfo  47429  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  spr0nelg  47463  sprel  47471  prelspr  47473  sprsymrelf1lem  47478  sprsymrelfolem2  47480  paireqne  47498  prprelb  47503  prprelprb  47504  reupr  47509  reuopreuprim  47513  fmtnoprmfac1lem  47551  fmtnofac2  47556  m1expevenALTV  47634  odd2np1ALTV  47661  opoeALTV  47670  opeoALTV  47671  perfectALTVlem2  47709  isgbe  47738  isgbow  47739  isgbo  47740  sbgoldbalt  47768  sgoldbeven3prm  47770  mogoldbb  47772  nnsum3primesgbe  47779  nnsum3primesle9  47781  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  vopnbgrel  47840  dfclnbgr6  47842  dfnbgr6  47843  isuspgrim0  47872  isuspgrimlem  47874  clnbgrgrim  47902  usgrgrtrirex  47917  stgredgel  47924  stgrusgra  47926  stgr1  47928  grlimgrtri  47963  gpgedgel  48007  uspgrsprf1  48063  uspgrsprfo  48064  0nodd  48086  1odd  48087  2nodd  48088  0even  48153  1neven  48154  2even  48155  2zlidl  48156  2zrngamgm  48161  2zrngagrp  48165  2zrngmmgm  48168  2zrngnmrid  48172  suppmptcfin  48292  lcoval  48329  linc0scn0  48340  linc1  48342  el0ldep  48383  snlindsntor  48388  blenval  48492  nn0sumshdiglemB  48541  itcoval1  48584  mo0  48733  oppcmndclem  48905  upciclem1  48923  isthincd2lem1  49075  termcbasmo  49128