Theorem eqeq1 2744

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 2742	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqeq1i  2745  eqeq12OLD  2759  eqtr  2763  eqtr2  2764  iseqsetvlem  2808  eqsb1  2870  cbvexeqsetf  3503  cgsex4gOLD  3539  sbhypfOLD  3557  rexraleqim  3660  eqvincf  3663  pm13.183  3679  moeq  3729  mob  3739  euind  3746  reu2eqd  3758  reuind  3775  eqsbc1  3854  sbceqal  3870  csbhypf  3950  uniiunlem  4110  snjust  4647  elsng  4662  elprg  4670  reusngf  4696  rexreusng  4703  reuprg0  4727  rabrsn  4749  preq12bg  4878  intab  5002  uniintsn  5009  dfiun2g  5053  dfiin2g  5055  disji2  5150  disjprg  5162  unopab  5248  eusv1  5409  reusv2lem2  5417  reusv3  5423  opthg  5497  copsexgw  5510  copsexg  5511  propeqop  5526  euotd  5532  otiunsndisj  5539  elopabw  5545  solin  5634  elxpi  5722  opbrop  5797  relop  5875  ideqg  5876  dmopab2rex  5942  elrnmpt  5981  elrnmpt1  5983  elrnmptg  5984  restidsing  6082  somin1  6165  cnveqb  6227  reu3op  6323  reuop  6324  ordequn  6498  iotaval2  6541  funopg  6612  f0rn0  6806  fvelrnb  6982  fvmptg  7027  fndmin  7078  eldmrexrn  7125  foelrn  7141  foelrnf  7142  foco2  7143  fmptco  7163  funopsn  7182  funsndifnop  7185  fmptsng  7202  fmptsnd  7203  tpres  7238  eufnfv  7266  elabrex  7279  elabrexg  7280  abrexco  7281  f1veqaeq  7294  fpropnf1  7304  nf1const  7340  isosolem  7383  f1oiso  7387  eusvobj2  7440  oprabidw  7479  oprabid  7480  f1opr  7506  oprabv  7510  0mpo0  7533  elrnmpog  7585  elrnmpo  7586  elrnmpores  7588  ralrnmpo  7589  ov3  7613  ov6g  7614  ovelrn  7626  caovcang  7651  caovcan  7654  uniuni  7797  orduninsuc  7880  funcnvuni  7972  fiunlem  7982  fiun  7983  f1iun  7984  f1oweALT  8013  opiota  8100  eloprabi  8104  frxp  8167  funsssuppss  8231  dftpos4  8286  tz7.44-2  8463  tz7.44-3  8464  oev  8570  oalimcl  8616  omlimcl  8634  odi  8635  omeu  8641  oeeui  8658  nneob  8712  omopth  8718  eldifsucnn  8720  elqsg  8826  qsdisj  8852  qsel  8854  brecop  8868  eroveu  8870  erovlem  8871  elixpsn  8995  ixpsnf1o  8996  boxcutc  8999  2dom  9095  fundmen  9096  xpf1o  9205  nneneq  9272  nneneqOLD  9284  fofinf1o  9400  elfi  9482  elfiun  9499  dffi3  9500  brwdom  9636  brwdom3  9651  unwdomg  9653  xpwdomg  9654  noinfep  9729  cantnfp1lem1  9747  cantnfp1lem3  9749  cantnflem1  9758  ssttrcl  9784  ttrclselem2  9795  scott0  9955  updjudhcoinrg  10002  updjud  10003  carden2a  10035  cardiun  10051  pm54.43lem  10069  alephval3  10179  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  dfac2b  10200  kmlem9  10228  kmlem12  10231  cardcf  10321  cfeq0  10325  cfsuc  10326  cff1  10327  cflim2  10332  cfss  10334  isfin5  10368  fin1a2lem11  10479  fin1a2lem13  10481  brdom7disj  10600  brdom6disj  10601  canthp1lem2  10722  canthp1  10723  tskuni  10852  gruina  10887  genpv  11068  genpelv  11069  addsrmo  11142  mulsrmo  11143  ltsosr  11163  ltresr  11209  axcnre  11233  axpre-lttri  11234  ltordlem  11815  ltord1  11816  fimaxre3  12241  supaddc  12262  supadd  12263  supmul1  12264  supmullem1  12265  supmullem2  12266  supmul  12267  creur  12287  creui  12288  nn1m1nn  12314  elz  12641  nn0ind-raph  12743  xnegeq  13269  xmullem2  13327  xmulasslem  13347  fleqceilz  13905  fseqsupubi  14029  sqeqor  14265  nn0opth2  14321  hash1snb  14468  hash2prde  14519  prprrab  14522  hash2pwpr  14525  tpf1ofv1  14546  tpf1ofv2  14547  tpfo  14549  fi1uzind  14556  wrd2ind  14771  cshfn  14838  cshf1  14858  2cshwcshw  14874  scshwfzeqfzo  14875  pfx2  14996  s3iunsndisj  15017  relexpsucnnr  15074  relexprelg  15087  rtrclreclem3  15109  shftfval  15119  sgnval  15137  01sqrexlem6  15296  reusq0  15511  summo  15765  fsum  15768  telfsumo  15850  infcvgaux1i  15905  infcvgaux2i  15906  mertenslem1  15932  mertenslem2  15933  mertens  15934  prodmo  15984  fprod  15989  ruclem12  16289  mod2eq1n2dvds  16395  divalg  16451  ndvdssub  16457  sadcp1  16501  smupp1  16526  gcdval  16542  bezoutlem1  16586  bezoutlem3  16588  bezoutlem4  16589  bezout  16590  lcmval  16639  coprmgcdb  16696  coprmdvds1  16699  divgcdcoprmex  16713  dvdsprime  16734  nprm  16735  dvdsprm  16750  coprm  16758  qnumval  16784  qdenval  16785  m1dvdsndvds  16845  reumodprminv  16851  pcval  16891  pceu  16893  pczpre  16894  pcdiv  16899  4sqlem2  16996  4sqlem4  16999  4sqlem12  17003  4sq  17011  vdwapval  17020  vdwapun  17021  vdwlem6  17033  cshwrepswhash1  17150  acsfn  17717  initoid  18068  termoid  18069  cat1lem  18163  posi  18387  gsumval2a  18723  smndex2dnrinv  18950  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  sgrp2nmndlem5  18964  mgmnsgrpex  18966  sgrpnmndex  18967  cyccom  19243  ghmf1  19286  conjnmzb  19293  orbsta  19353  symgextfv  19460  symgextfo  19464  symgfixfo  19481  pmtrprfval  19529  pmtrprfvalrn  19530  psgneu  19548  psgnval  19549  psgnvali  19550  psgnvalii  19551  odfval  19574  odval  19576  dfod2  19606  submod  19611  isslw  19650  sylow2alem1  19659  sylow3lem2  19670  lsmelvalm  19693  lsmdisj2  19724  efgrelexlemb  19792  frgpup3lem  19819  cyggeninv  19925  gsumval3eu  19946  gsumval3lem2  19948  gsummpt1n0  20007  nn0gsumfz  20026  dprddisj2  20083  dpjrid  20106  pgpfac1lem3  20121  rrgeq0i  20721  domneq0  20730  domnlcanb  20742  domnrcanb  20744  abveq0  20841  abvtrivd  20855  lss1d  20984  lspsn  21023  ellspsn  21024  lspprel  21116  prmirredlem  21506  znf1o  21593  znfld  21602  znunit  21605  cygznlem3  21611  psgndif  21643  ipeq0  21679  obsip  21764  frlmphl  21824  uvcvval  21829  ellspd  21845  psrlidm  22005  psrridm  22006  psrascl  22022  mvrval2  22026  mvrf1  22029  mplmonmul  22077  evlslem3  22127  mhpsclcl  22174  psdmplcl  22189  psdmul  22193  coe1tm  22297  coe1tmfv2  22299  cply1coe0  22326  cply1coe0bi  22327  gsummoncoe1  22333  mamufacex  22421  mat1comp  22467  mat1dimelbas  22498  mat1dimid  22501  scmatel  22532  scmateALT  22539  mavmulsolcl  22578  marrepeval  22590  marepveval  22595  mdetunilem8  22646  maducoeval2  22667  madugsum  22670  minmar1eval  22676  symgmatr01lem  22680  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  m2cpm  22768  m2cpminvid2lem  22781  decpmatid  22797  monmatcollpw  22806  pmatcollpw3fi1lem1  22813  mp2pm2mplem4  22836  fvmptnn04ifc  22879  chfacffsupp  22883  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  cpmadumatpoly  22910  cayleyhamilton  22917  cayleyhamiltonALT  22918  istopon  22939  toponsspwpw  22949  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  epttop  23037  t0sep  23353  t1sep2  23398  cmpsublem  23428  cmpsub  23429  unisngl  23556  txuni2  23594  elpt  23601  ptbasfi  23610  xkoopn  23618  ptpjopn  23641  ptclsg  23644  dfac14lem  23646  ptcnp  23651  ptrescn  23668  tx1stc  23679  qtopeu  23745  kqt0lem  23765  isr0  23766  hauspwpwf1  24016  xmeteq0  24369  imasf1oxmet  24406  comet  24547  stdbdxmet  24549  met2ndci  24556  prdsxmslem2  24563  nrmmetd  24608  tngngp  24696  tngngp3  24698  xrsxmet  24850  iccpnfcnv  24994  iccpnfhmeo  24995  cnheibor  25006  elovolm  25529  ovolgelb  25534  ovolicc1  25570  ovolicc  25577  ioorval  25628  uniioombllem6  25642  dyadmax  25652  dyadmbl  25654  i1fadd  25749  i1fmul  25750  itg1addlem3  25752  i1fmulc  25758  itg2l  25784  itg2leub  25789  limcmpt  25938  limcco  25948  dvcobr  26003  dvcobrOLD  26004  deg1ldg  26151  ig1pval  26235  elply  26254  elply2  26255  coeval  26282  coe1termlem  26317  coe1term  26318  quotval  26352  plydivlem4  26356  plydivex  26357  vieta1  26372  aannenlem2  26389  aalioulem2  26393  abelthlem9  26502  logtayllem  26719  logtayl  26720  isosctrlem2  26880  leibpilem2  27002  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  mpodvdsmulf1o  27255  dvdsmulf1o  27257  perfectlem2  27292  lgsfval  27364  lgsval2lem  27369  lgsqrmodndvds  27415  lgsdchrval  27416  gausslemma2dlem0i  27426  2lgslem1b  27454  2lgslem3  27466  2sqlem2  27480  2sqlem8  27488  2sqlem9  27489  2sqlem11  27491  addsq2reu  27502  dchrisum0flblem1  27570  padicval  27679  padicabv  27692  ostth1  27695  sltval2  27719  sltintdifex  27724  sltres  27725  nolt02o  27758  madef  27913  addsval2  28014  addsproplem2  28021  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  addsprop  28027  addscut  28029  sleadd1  28040  addsuniflem  28052  addsunif  28053  addsasslem1  28054  addsasslem2  28055  addsbdaylem  28067  negsprop  28085  negsid  28091  mulsval2lem  28154  mulsproplem9  28168  mulsproplem12  28171  mulsprop  28174  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  mulsunif2  28214  precsexlemcbv  28248  precsexlem9  28257  precsexlem11  28259  n0s0suc  28363  n0s0m1  28377  n0seo  28423  zseo  28424  expsval  28426  elzs12  28439  recut  28446  0reno  28447  renegscl  28448  readdscl  28449  remulscllem1  28450  remulscl  28452  axtgcgrid  28489  axtgbtwnid  28492  islmib  28813  inaghl  28871  axpaschlem  28973  axlowdimlem15  28989  axlowdim  28994  upgredg2vtx  29176  edglnl  29178  umgredgnlp  29182  usgredg2vtxeuALT  29257  uspgredg2v  29259  ushgredgedgloop  29266  nbusgredgeu  29401  cusgrfilem2  29492  cusgrfi  29494  vtxdushgrfvedg  29526  1loopgrvd2  29539  rusgr1vtxlem  29623  wlkeq  29670  wlkp1lem8  29716  upgrwlkdvdelem  29772  crctcshwlkn0lem6  29848  wlknwwlksnbij  29921  rusgrnumwwlkl1  30001  clwlkclwwlklem2a1  30024  clwwlknscsh  30094  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknon1sn  30132  frgr3vlem1  30305  3vfriswmgrlem  30309  frgrncvvdeqlem3  30333  wlkl0  30399  frgrreggt1  30425  nvz  30701  nmosetn0  30797  nmoolb  30803  nmoubi  30804  nmlno0lem  30825  nmlno0i  30826  hvsubeq0  31100  hvaddcan  31102  normsub0  31168  norm1exi  31282  pjhval  31429  omlsii  31435  omlsi  31436  pjoml  31468  h1de2ci  31588  spansneleq  31602  h1datomi  31613  h1datom  31614  spansncv  31685  5oalem6  31691  pj11  31746  nmopsetn0  31897  nmfnsetn0  31910  nmoplb  31939  nmopub  31940  nmfnlb  31956  nmfnleub  31957  nmlnop0iALT  32027  nmlnop0  32030  lnopeq  32041  nmopun  32046  nmcexi  32058  branmfn  32137  pjnmopi  32180  pj3i  32240  atss  32378  atom1d  32385  chirred  32427  cdj3lem2  32467  eqelbid  32503  elabreximd  32538  disjxpin  32610  disjunsn  32616  br8d  32632  fmptcof2  32675  psgnfzto1stlem  33093  sgnsval  33154  domnlcanOLD  33249  linds2eq  33374  elrspunsn  33422  mxidlmax  33458  1arithidomlem1  33528  1arithidom  33530  1arithufdlem1  33537  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  1arithufd  33541  dfufd2  33543  ply1dg1rt  33569  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  rtelextdg2lem  33717  constrsuc  33728  2sqr3minply  33738  madjusmdetlem2  33774  madjusmdet  33777  zarclssn  33819  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iifhom  33883  xrge0tmd  33891  xrge0tmdALT  33892  esumc  34015  sgn3da  34506  sgnmul  34507  sgnnbi  34510  sgnpbi  34511  sgn0bi  34512  plymulx0  34524  signspval  34529  tgoldbachgt  34640  bnj1468  34822  f1resfz0f1d  35081  acycgrcycl  35115  sconnpi1  35207  cvmlift3lem2  35288  satfv0  35326  satfv1  35331  satfbrsuc  35334  satfrnmapom  35338  satfv0fun  35339  satf0op  35345  sat1el2xp  35347  fmlafvel  35353  fmla1  35355  isfmlasuc  35356  fmlaomn0  35358  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  fmla0disjsuc  35366  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem2lem1  35372  dmopab3rexdif  35373  satfv0fvfmla0  35381  sategoelfvb  35387  ex-sategoelel  35389  satfv1fvfmla1  35391  2goelgoanfmla1  35392  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  prv1n  35399  ellcsrspsn  35609  r1peuqusdeg1  35611  br8  35718  br6  35719  br4  35720  rdgprc0  35757  dfrdg2  35759  dfbigcup2  35863  elsingles  35882  dfiota3  35887  brimageg  35891  brdomaing  35899  brrangeg  35900  dfrdg4  35915  elaltxp  35939  funtransport  35995  fvtransport  35996  brsegle  36072  funray  36104  fvray  36105  funline  36106  fvline  36108  ellines  36116  linethru  36117  rankeq1o  36135  subtr  36280  subtr2  36281  nn0prpw  36289  bj-elabd2ALT  36891  bj-gabss  36901  bj-imafv  37217  topdifinffinlem  37313  topdifinffin  37314  topdifinfeq  37316  finxpreclem2  37356  finxpreclem3  37359  fvineqsnf1  37376  fvineqsneu  37377  wl-issetft  37536  fin2so  37567  ptrest  37579  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anc  37661  unirep  37674  sdclem2  37702  sdclem1  37703  sdc  37704  fdc  37705  isbnd  37740  heibor1lem  37769  heiborlem4  37774  heiborlem6  37776  heiborlem10  37780  ismgmOLD  37810  maxidlmax  38003  prnc  38027  isfldidl  38028  dmnnzd  38035  disjressuc2  38344  qsdisjALTV  38571  eqvrelqsel  38572  riotasvd  38912  lshpdisj  38943  lsat0cv  38989  lcvexchlem4  38993  lcvexchlem5  38994  lshpkrlem1  39066  lshpkrlem2  39067  lshpkrlem3  39068  lshpkrcl  39072  islshpkrN  39076  atnle  39273  glbconxN  39335  isline  39696  ispointN  39699  pmapglbx  39726  ispsubcl2N  39904  lhp2atnle  39990  cdleme43fsv1snlem  40377  cdleme40v  40426  cdlemkid5  40892  cdlemkid  40893  dvhb1dimN  40943  dib1dim  41122  dicopelval  41134  dicelval1sta  41144  diclspsn  41151  dihvalcqpre  41192  dihglblem2aN  41250  dihglblem2N  41251  dih1dimatlem  41286  dihpN  41293  dochfl1  41433  lcfl7N  41458  lcf1o  41508  hvmapvalvalN  41718  hdmapval2lem  41788  aks6d1c1  42073  aks6d1c4  42081  sticksstones10  42112  sticksstones12a  42114  aks6d1c7  42141  metakunt3  42164  metakunt4  42165  metakunt6  42167  metakunt7  42168  metakunt8  42169  metakunt10  42171  metakunt11  42172  metakunt12  42173  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt24  42185  sn-iotalem  42214  f1o2d2  42228  fiabv  42491  evlsbagval  42521  selvvvval  42540  fsuppind  42545  absnw  42633  elrfi  42650  nacsfg  42661  mzpcompact2lem  42707  eldioph2b  42719  eldioph3  42722  eldiophss  42730  diophrex  42731  elnn0rabdioph  42759  rencldnfilem  42776  elpell1qr  42803  elpell14qr  42805  elpell1234qr  42807  jm2.27  42965  rmydioph  42971  expdiophlem2  42979  wepwsolem  42999  aomclem6  43016  lnr2i  43073  lpirlnr  43074  hbtlem2  43081  hbtlem4  43083  hbtlem5  43085  rngunsnply  43130  flcidc  43131  onsucelab  43225  limnsuc  43227  nnoeomeqom  43274  cantnfresb  43286  tfsconcatfv2  43302  tfsconcatb0  43306  oaun3lem1  43336  oadif1lem  43341  oadif1  43342  clcnvlem  43585  brtrclfv2  43689  frege55lem1c  43878  frege104  43929  clsk1indlem0  44003  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  clsk1indlem1  44007  pm13.192  44379  equncomVD  44839  csbingVD  44855  csbsngVD  44864  csbfv12gALTVD  44870  relopabVD  44872  refsum2cnlem1  44937  elrnmptf  45088  upbdrech  45220  ssfiunibd  45224  iccshift  45436  iooshift  45440  fsumf1of  45495  limcperiod  45549  climinf2mpt  45635  climinfmpt  45636  cncfshiftioo  45813  itgiccshift  45901  itgperiod  45902  stoweidlem46  45967  fourierdlem29  46057  fourierdlem37  46065  fourierdlem48  46075  fourierdlem51  46078  fourierdlem54  46081  fourierdlem62  46089  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem92  46119  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem103  46130  fourierdlem104  46131  fourierdlem105  46132  fourierdlem108  46135  fourierdlem110  46137  fourierdlem112  46139  etransclem1  46156  etransclem5  46160  etransclem17  46172  etransclem32  46187  etransclem41  46196  sge0f1o  46303  sge0resplit  46327  sge0fodjrnlem  46337  nnfoctbdjlem  46376  nnfoctbdj  46377  ovnval  46462  ovnlecvr  46479  ovnpnfelsup  46480  ovn0lem  46486  hoidmvval  46498  hoidmvlelem1  46516  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  hoidifhspval3  46540  hspmbllem2  46548  hoimbl  46552  ovnsubadd2  46567  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovol  46580  fsetsnf  46966  fsetsnfo  46968  fcoresf1  46984  aiotaval  47010  euoreqb  47024  afv0fv0  47064  afvfv0bi  47067  afvelrnb  47078  afvelrnb0  47079  afv20defat  47147  otiunsndisjX  47194  fun2dmnopgexmpl  47199  2ffzoeq  47242  elsetpreimafvb  47258  imasetpreimafvbijlemfo  47279  fargshiftf1  47315  fargshiftfo  47316  ichnreuop  47346  ichreuopeq  47347  elsprel  47349  spr0nelg  47350  sprel  47358  prelspr  47360  sprsymrelf1lem  47365  sprsymrelfolem2  47367  paireqne  47385  prprelb  47390  prprelprb  47391  reupr  47396  reuopreuprim  47400  fmtnoprmfac1lem  47438  fmtnofac2  47443  m1expevenALTV  47521  odd2np1ALTV  47548  opoeALTV  47557  opeoALTV  47558  perfectALTVlem2  47596  isgbe  47625  isgbow  47626  isgbo  47627  sbgoldbalt  47655  sgoldbeven3prm  47657  mogoldbb  47659  nnsum3primesgbe  47666  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  isuspgrim0  47756  isuspgrimlem  47758  clnbgrgrim  47786  usgrgrtrirex  47799  grlimgrtri  47820  uspgrsprf1  47870  uspgrsprfo  47871  0nodd  47893  1odd  47894  2nodd  47895  0even  47960  1neven  47961  2even  47962  2zlidl  47963  2zrngamgm  47968  2zrngagrp  47972  2zrngmmgm  47975  2zrngnmrid  47979  suppmptcfin  48104  lcoval  48141  linc0scn0  48152  linc1  48154  el0ldep  48195  snlindsntor  48200  blenval  48305  nn0sumshdiglemB  48354  itcoval1  48397  mo0  48545  isthincd2lem1  48694