Theorem eqeq1 2773

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2771	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqeq1i  2774  eqtr  2789  eqtr2  2790  iseqsetvlem  2832  eqsb1  2895  cbvexeqsetf  3478  rexraleqim  3615  eqvincf  3618  pm13.183  3634  moeq  3679  mob  3689  euind  3696  reu2eqd  3708  reuind  3725  eqsbc1  3799  sbceqal  3814  csbhypf  3889  uniiunlem  4049  snjust  4593  elsng  4608  elprg  4617  reusngf  4645  rexreusng  4650  reuprg0  4673  rabrsn  4695  preq12bg  4822  intab  4947  uniintsn  4954  dfiun2g  4998  dfiin2g  4999  disji2  5097  disjprg  5109  unopab  5195  eusv1  5363  reusv2lem2  5371  reusv3  5377  axprg  5409  opthg  5460  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  propeqop  5491  euotd  5497  otiunsndisj  5504  elopabw  5511  solin  5597  elxpi  5684  opbrop  5760  relop  5837  ideqg  5838  dmopab2rex  5908  elrnmpt  5949  elrnmpt1  5951  elrnmptg  5952  restidsing  6056  somin1  6134  cnveqb  6196  reu3op  6294  reuop  6295  ordequn  6467  iotaval2  6508  funopg  6571  f0rn0  6764  fvelrnb  6942  fvmptg  6988  fndmin  7041  eldmrexrn  7087  foelrn  7103  foelrnf  7104  foco2  7105  fmptco  7126  funopsn  7145  funopsnOLD  7146  funsndifnop  7149  fmptsng  7167  fmptsnd  7168  tpres  7200  eufnfv  7228  elabrex  7241  elabrexg  7242  abrexco  7243  f1veqaeq  7255  fpropnf1  7266  nf1const  7303  isosolem  7346  f1oiso  7350  eusvobj2  7403  oprabidw  7442  oprabid  7443  f1opr  7467  oprabv  7471  0mpo0  7494  elrnmpog  7546  elrnmpo  7547  elrnmpores  7549  ralrnmpo  7550  ov3  7574  ov6g  7575  ovelrn  7587  caovcang  7612  caovcan  7615  caofidlcan  7713  uniuni  7761  orduninsuc  7839  funcnvuni  7929  fiunlem  7939  fiun  7940  f1iun  7941  f1oweALT  7969  opiota  8056  eloprabi  8060  mpof1o2d  8121  frxp  8122  funsssuppss  8186  dftpos4  8241  tz7.44-2  8394  tz7.44-3  8395  oev  8499  oalimcl  8545  omlimcl  8563  odi  8564  omeu  8570  oeeui  8588  nneob  8642  omopth  8648  eldifsucnn  8650  elqsg  8761  qsdisj  8792  qsel  8794  brecop  8808  eroveu  8810  erovlem  8811  elixpsn  8935  ixpsnf1o  8936  boxcutc  8939  2dom  9027  fundmen  9028  xpf1o  9127  nneneq  9190  fofinf1o  9289  elfi  9373  elfiun  9390  dffi3  9391  brwdom  9529  brwdom3  9544  unwdomg  9546  xpwdomg  9547  noinfep  9629  cantnfp1lem1  9647  cantnfp1lem3  9649  cantnflem1  9658  ssttrcl  9684  ttrclselem2  9695  scott0  9860  updjudhcoinrg  9919  updjud  9920  carden2a  9952  cardiun  9968  pm54.43lem  9986  alephval3  10094  dfac5lem3  10109  dfac5lem4  10110  dfac2b  10114  kmlem9  10142  kmlem12  10145  cardcf  10235  cfeq0  10240  cfsuc  10241  cff1  10242  cflim2  10247  cfss  10249  isfin5  10283  fin1a2lem11  10394  fin1a2lem13  10396  brdom7disj  10515  brdom6disj  10516  canthp1lem2  10638  canthp1  10639  tskuni  10768  gruina  10803  genpv  10984  genpelv  10985  addsrmo  11058  mulsrmo  11059  ltsosr  11079  ltresr  11125  axcnre  11149  axpre-lttri  11150  ltordlem  11739  ltord1  11740  fimaxre3  12161  supaddc  12182  supadd  12183  supmul1  12184  supmullem1  12185  supmullem2  12186  supmul  12187  creur  12212  creui  12213  nn1m1nn  12254  elz  12593  nn0ind-raph  12696  xnegeq  13233  xmullem2  13291  xmulasslem  13311  fleqceilz  13887  fseqsupubi  14014  sqeqor  14252  nn0opth2  14308  hash1snb  14456  hash2prde  14507  prprrab  14510  hash2pwpr  14513  tpf1ofv1  14534  tpf1ofv2  14535  tpfo  14537  fi1uzind  14544  wrd2ind  14760  cshfn  14827  cshf1  14847  2cshwcshw  14862  scshwfzeqfzo  14863  pfx2  14984  s3iunsndisj  15005  relexpsucnnr  15062  relexprelg  15075  rtrclreclem3  15097  shftfval  15107  sgnval  15125  sgn3da  15138  sgn0bi  15140  sgnnbi  15141  sgnpbi  15142  sgnmul  15144  01sqrexlem6  15298  reusq0  15516  summo  15768  fsum  15771  telfsumo  15854  infcvgaux1i  15911  infcvgaux2i  15912  mertenslem1  15938  mertenslem2  15939  mertens  15940  prodmo  15990  fprod  15995  ruclem12  16297  mod2eq1n2dvds  16405  divalg  16461  ndvdssub  16467  sadcp1  16513  smupp1  16538  gcdval  16554  bezoutlem1  16597  bezoutlem3  16599  bezoutlem4  16600  bezout  16601  lcmval  16650  coprmgcdb  16707  coprmdvds1  16710  divgcdcoprmex  16724  dvdsprime  16745  nprm  16746  dvdsprm  16762  coprm  16770  qnumval  16796  qdenval  16797  m1dvdsndvds  16858  reumodprminv  16864  pcval  16904  pceu  16906  pczpre  16907  pcdiv  16912  4sqlem2  17009  4sqlem4  17012  4sqlem12  17016  4sq  17024  vdwapval  17033  vdwapun  17034  vdwlem6  17046  cshwrepswhash1  17162  acsfn  17715  initoid  18058  termoid  18059  cat1lem  18153  posi  18373  gsumval2a  18743  smndex2dnrinv  18977  mgm2nsgrplem2  18981  mgm2nsgrplem3  18982  sgrp2nmndlem5  18991  mgmnsgrpex  18993  sgrpnmndex  18994  cyccom  19274  ghmf1  19316  conjnmzb  19323  orbsta  19383  symgextfv  19488  symgextfo  19492  symgfixfo  19509  pmtrprfval  19557  pmtrprfvalrn  19558  psgneu  19576  psgnval  19577  psgnvali  19578  psgnvalii  19579  odfval  19602  odval  19604  dfod2  19634  submod  19639  isslw  19678  sylow2alem1  19687  sylow3lem2  19698  lsmelvalm  19721  lsmdisj2  19752  efgrelexlemb  19820  frgpup3lem  19847  cyggeninv  19953  gsumval3eu  19974  gsumval3lem2  19976  gsummpt1n0  20035  nn0gsumfz  20054  dprddisj2  20111  dpjrid  20134  pgpfac1lem3  20149  rrgeq0i  20784  domneq0  20793  domnlcanb  20804  domnrcanb  20806  abveq0  20899  abvtrivd  20913  lss1d  21062  lspsn  21101  ellspsn  21102  lspprel  21193  prmirredlem  21591  znf1o  21670  znfld  21679  znunit  21682  cygznlem3  21688  psgndif  21721  ipeq0  21757  obsip  21840  frlmphl  21900  uvcvval  21905  ellspd  21921  psrlidm  22080  psrridm  22081  psrascl  22097  mvrval2  22101  mvrf1  22104  mplmonmul  22156  evlslem3  22200  selvvvval  22262  mhpsclcl  22279  psdmplcl  22294  psdmul  22298  psdmvr  22301  coe1tm  22403  coe1tmfv2  22405  cply1coe0  22430  cply1coe0bi  22431  gsummoncoe1  22437  mamufacex  22522  mat1comp  22566  mat1dimelbas  22597  mat1dimid  22600  scmatel  22631  scmateALT  22638  mavmulsolcl  22677  marrepeval  22689  marepveval  22694  mdetunilem8  22745  maducoeval2  22766  madugsum  22769  minmar1eval  22775  symgmatr01lem  22779  symgmatr01  22780  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  m2cpm  22867  m2cpminvid2lem  22880  decpmatid  22896  monmatcollpw  22905  pmatcollpw3fi1lem1  22912  mp2pm2mplem4  22935  fvmptnn04ifc  22978  chfacffsupp  22982  chfacfscmul0  22984  chfacfscmulgsum  22986  chfacfpmmul0  22988  chfacfpmmulgsum  22990  cpmadumatpoly  23009  cayleyhamilton  23016  cayleyhamiltonALT  23017  istopon  23038  toponsspwpw  23048  fctop  23130  cctop  23132  ppttop  23133  pptbas  23134  epttop  23135  t0sep  23450  t1sep2  23495  cmpsublem  23525  cmpsub  23526  unisngl  23653  txuni2  23691  elpt  23698  ptbasfi  23707  xkoopn  23715  ptpjopn  23738  ptclsg  23741  dfac14lem  23743  ptcnp  23748  ptrescn  23765  tx1stc  23776  qtopeu  23842  kqt0lem  23862  isr0  23863  hauspwpwf1  24113  xmeteq0  24464  imasf1oxmet  24501  comet  24639  stdbdxmet  24641  met2ndci  24648  prdsxmslem2  24655  nrmmetd  24700  tngngp  24780  tngngp3  24782  xrsxmet  24936  iccpnfcnv  25072  iccpnfhmeo  25073  cnheibor  25083  elovolm  25603  ovolgelb  25608  ovolicc1  25644  ovolicc  25651  ioorval  25702  uniioombllem6  25716  dyadmax  25726  dyadmbl  25728  i1fadd  25823  i1fmul  25824  itg1addlem3  25826  i1fmulc  25831  itg2l  25857  itg2leub  25862  limcmpt  26011  limcco  26021  dvcobr  26074  deg1ldg  26218  ig1pval  26302  elply  26321  elply2  26322  coeval  26349  coe1termlem  26384  coe1term  26385  plyn0mulidp  26411  quotval  26422  plydivlem4  26426  plydivex  26427  vieta1  26442  aannenlem2  26459  aalioulem2  26463  abelthlem9  26569  logtayllem  26790  logtayl  26791  isosctrlem2  26950  leibpilem2  27072  rlimcnp2  27097  efrlim  27100  mpodvdsmulf1o  27324  dvdsmulf1o  27326  perfectlem2  27360  lgsfval  27432  lgsval2lem  27437  lgsqrmodndvds  27483  lgsdchrval  27484  gausslemma2dlem0i  27494  2lgslem1b  27522  2lgslem3  27534  2sqlem2  27548  2sqlem8  27556  2sqlem9  27557  2sqlem11  27559  addsq2reu  27570  dchrisum0flblem1  27638  padicval  27747  padicabv  27760  ostth1  27763  ltsval2  27786  ltsintdifex  27791  ltsres  27792  nolt02o  27825  madef  27995  addsval2  28122  addsproplem2  28129  addsproplem4  28131  addsproplem5  28132  addsproplem6  28133  addsprop  28135  addcuts  28137  leadds1  28148  addsuniflem  28160  addsunif  28161  addsasslem1  28162  addsasslem2  28163  addbdaylem  28176  negsprop  28194  negsid  28200  mulsval2lem  28269  mulsproplem9  28283  mulsproplem12  28286  mulsprop  28289  sltmuls1  28306  sltmuls2  28307  mulsuniflem  28308  addsdilem1  28310  addsdilem2  28311  mulsasslem1  28322  mulsasslem2  28323  mulsunif2  28329  precsexlemcbv  28365  precsexlem9  28374  precsexlem11  28376  n0s0suc  28501  onsfi  28515  n0s0m1  28521  nn1m1nns  28533  eucliddivs  28535  n0seo  28580  zseo  28581  expsval  28584  bdayfinbndcbv  28625  bdayfinbndlem1  28626  bdayfinbndlem2  28627  bdayfinbnd  28628  elz12s  28631  z12zsodd  28641  z12sge0  28642  recut  28653  elreno2  28654  renegscl  28657  readdscl  28658  remulscllem1  28659  remulscl  28661  axtgcgrid  28698  axtgbtwnid  28701  islmib  29054  inaghl  29117  axpaschlem  29231  axlowdimlem15  29247  axlowdim  29252  upgredg2vtx  29432  edglnl  29434  umgredgnlp  29438  usgredg2vtxeuALT  29513  uspgredg2v  29515  ushgredgedgloop  29522  nbusgredgeu  29657  cusgrfilem2  29747  cusgrfi  29749  vtxdushgrfvedg  29781  1loopgrvd2  29794  rusgr1vtxlem  29878  wlkeq  29924  wlkp1lem8  29969  upgrwlkdvdelem  30026  crctcshwlkn0lem6  30105  wlknwwlksnbij  30178  rusgrnumwwlkl1  30261  clwlkclwwlklem2a1  30284  clwwlknscsh  30354  eleclclwwlkn  30368  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  clwwlknon1sn  30392  frgr3vlem1  30565  3vfriswmgrlem  30569  frgrncvvdeqlem3  30593  wlkl0  30659  frgrreggt1  30685  nvz  30962  nmosetn0  31058  nmoolb  31064  nmoubi  31065  nmlno0lem  31086  nmlno0i  31087  hvsubeq0  31361  hvaddcan  31363  normsub0  31429  norm1exi  31543  pjhval  31690  omlsii  31696  omlsi  31697  pjoml  31729  h1de2ci  31849  spansneleq  31863  h1datomi  31874  h1datom  31875  spansncv  31946  5oalem6  31952  pj11  32007  nmopsetn0  32158  nmfnsetn0  32171  nmoplb  32200  nmopub  32201  nmfnlb  32217  nmfnleub  32218  nmlnop0iALT  32288  nmlnop0  32291  lnopeq  32302  nmopun  32307  nmcexi  32319  branmfn  32398  pjnmopi  32441  pj3i  32501  atss  32639  atom1d  32646  chirred  32688  cdj3lem2  32728  eqelbid  32762  elabreximd  32797  disjxpin  32874  disjunsn  32880  br8d  32894  fmptcof2  32943  psgnfzto1stlem  33361  sgnsval  33422  elrgspnlem2  33504  elrgspnlem3  33505  linds2eq  33638  elrspunsn  33681  mxidlmax  33693  1arithidomlem1  33770  1arithidom  33772  1arithufdlem1  33779  1arithufdlem2  33780  1arithufdlem3  33781  1arithufdlem4  33782  1arithufd  33783  dfufd2  33785  ply1dg1rt  33815  selvply1rhmlem2  33856  mplvrpmrhm  33882  psrmonmul  33885  esplyfvaln  33909  lbsdiflsp0  33961  fedgmullem1  33964  fedgmullem2  33965  rtelextdg2lem  34061  constrsuc  34073  constrcbvlem  34090  2sqr3minply  34115  madjusmdetlem2  34163  madjusmdet  34166  zarclssn  34208  xrge0iifcnv  34268  xrge0iifcv  34269  xrge0iifhom  34272  xrge0tmd  34280  xrge0tmdALT  34281  esumc  34386  signspval  34884  tgoldbachgt  34995  bnj1468  35179  fineqvnttrclselem3  35459  fineqvnttrclse  35460  f1resfz0f1d  35504  acycgrcycl  35538  sconnpi1  35630  cvmlift3lem2  35711  satfv0  35749  satfv1  35754  satfbrsuc  35757  satfrnmapom  35761  satfv0fun  35762  satf0op  35768  sat1el2xp  35770  fmlafvel  35776  fmla1  35778  isfmlasuc  35779  fmlaomn0  35781  gonan0  35783  goaln0  35784  gonar  35786  goalr  35788  fmla0disjsuc  35789  fmlasucdisj  35790  satffunlem1lem1  35793  satffunlem2lem1  35795  dmopab3rexdif  35796  satfv0fvfmla0  35804  sategoelfvb  35810  ex-sategoelel  35812  satfv1fvfmla1  35814  2goelgoanfmla1  35815  ex-sategoelelomsuc  35817  ex-sategoelel12  35818  prv1n  35822  ellcsrspsn  36032  r1peuqusdeg1  36034  br8  36147  br6  36148  br4  36149  rdgprc0  36182  dfrdg2  36184  dfbigcup2  36288  elsingles  36307  dfiota3  36312  brimageg  36316  brdomaing  36324  brrangeg  36325  dfrdg4  36342  elaltxp  36366  funtransport  36422  fvtransport  36423  brsegle  36499  funray  36531  fvray  36532  funline  36533  fvline  36535  ellines  36543  linethru  36544  rankeq1o  36562  subtr  36714  subtr2  36715  nn0prpw  36723  bj-elabd2ALT  37449  bj-gabss  37459  bj-imafv  37783  topdifinffinlem  37881  topdifinffin  37882  topdifinfeq  37884  finxpreclem2  37924  finxpreclem3  37927  fvineqsnf1  37944  fvineqsneu  37945  wl-ax12v2cl  38040  wl-dfclel  38049  wl-issetft  38125  fin2so  38146  ptrest  38158  poimirlem25  38184  poimirlem26  38185  poimirlem27  38186  poimirlem28  38187  poimirlem31  38190  poimirlem32  38191  heicant  38194  mblfinlem2  38197  mblfinlem3  38198  mblfinlem4  38199  ismblfin  38200  itg2addnclem  38210  itg2addnclem3  38212  itg2addnc  38213  ftc1anc  38240  unirep  38253  sdclem2  38281  sdclem1  38282  sdc  38283  fdc  38284  isbnd  38319  heibor1lem  38348  heiborlem4  38353  heiborlem6  38355  heiborlem10  38359  ismgmOLD  38389  maxidlmax  38582  prnc  38606  isfldidl  38607  dmnnzd  38614  disjressuc2  38950  qsdisjALTV  39238  eqvrelqsel  39239  riotasvd  39620  lshpdisj  39651  lsat0cv  39697  lcvexchlem4  39701  lcvexchlem5  39702  lshpkrlem1  39774  lshpkrlem2  39775  lshpkrlem3  39776  lshpkrcl  39780  islshpkrN  39784  atnle  39981  glbconxN  40042  isline  40403  ispointN  40406  pmapglbx  40433  ispsubcl2N  40611  lhp2atnle  40697  cdleme43fsv1snlem  41084  cdleme40v  41133  cdlemkid5  41599  cdlemkid  41600  dvhb1dimN  41650  dib1dim  41829  dicopelval  41841  dicelval1sta  41851  diclspsn  41858  dihvalcqpre  41899  dihglblem2aN  41957  dihglblem2N  41958  dih1dimatlem  41993  dihpN  42000  dochfl1  42140  lcfl7N  42165  lcf1o  42215  hvmapvalvalN  42425  hdmapval2lem  42495  aks6d1c1  42773  aks6d1c4  42781  sticksstones10  42812  sticksstones12a  42814  aks6d1c7  42841  sn-iotalem  42882  fiabv  43196  evlsbagval  43210  fsuppind  43214  absnw  43302  elrfi  43317  nacsfg  43328  mzpcompact2lem  43374  eldioph2b  43386  eldioph3  43389  eldiophss  43397  diophrex  43398  elnn0rabdioph  43422  rencldnfilem  43439  elpell1qr  43466  elpell14qr  43468  elpell1234qr  43470  jm2.27  43627  rmydioph  43633  expdiophlem2  43641  wepwsolem  43661  aomclem6  43678  lnr2i  43735  lpirlnr  43736  hbtlem2  43743  hbtlem4  43745  hbtlem5  43747  rngunsnply  43788  flcidc  43789  onsucelab  43882  limnsuc  43884  nnoeomeqom  43931  cantnfresb  43943  tfsconcatfv2  43959  tfsconcatb0  43963  oaun3lem1  43993  oadif1lem  43998  oadif1  43999  clcnvlem  44241  brtrclfv2  44345  frege55lem1c  44534  frege104  44585  clsk1indlem0  44659  clsk1indlem2  44660  clsk1indlem3  44661  clsk1indlem4  44662  clsk1indlem1  44663  pm13.192  45012  equncomVD  45468  csbingVD  45484  csbsngVD  45493  csbfv12gALTVD  45499  relopabVD  45501  refsum2cnlem1  45649  elrnmptf  45791  upbdrech  45916  ssfiunibd  45920  iccshift  46126  iooshift  46130  fsumf1of  46182  limcperiod  46236  climinf2mpt  46320  climinfmpt  46321  cncfshiftioo  46498  itgiccshift  46586  itgperiod  46587  stoweidlem46  46652  fourierdlem29  46742  fourierdlem37  46750  fourierdlem48  46760  fourierdlem51  46763  fourierdlem54  46766  fourierdlem62  46774  fourierdlem79  46791  fourierdlem81  46793  fourierdlem82  46794  fourierdlem92  46804  fourierdlem96  46808  fourierdlem97  46809  fourierdlem98  46810  fourierdlem99  46811  fourierdlem103  46815  fourierdlem104  46816  fourierdlem105  46817  fourierdlem108  46820  fourierdlem110  46822  fourierdlem112  46824  etransclem1  46841  etransclem5  46845  etransclem17  46857  etransclem32  46872  etransclem41  46881  sge0f1o  46988  sge0resplit  47012  sge0fodjrnlem  47022  nnfoctbdjlem  47061  nnfoctbdj  47062  ovnval  47147  ovnlecvr  47164  ovnpnfelsup  47165  ovn0lem  47171  hoidmvval  47183  hoidmvlelem1  47201  ovnhoilem1  47207  ovnhoi  47209  ovnlecvr2  47216  hoidifhspval3  47225  hspmbllem2  47233  hoimbl  47237  ovnsubadd2  47252  ovolval5lem2  47259  ovolval5lem3  47260  ovolval5  47261  ovnovol  47265  sinnpoly  47517  fsetsnf  47677  fsetsnfo  47679  fcoresf1  47695  aiotaval  47721  euoreqb  47735  afv0fv0  47775  afvfv0bi  47778  afvelrnb  47789  afvelrnb0  47790  afv20defat  47858  otiunsndisjX  47905  fun2dmnopgexmpl  47910  2ffzoeq  47954  modmkpkne  47993  elsetpreimafvb  48022  imasetpreimafvbijlemfo  48043  fargshiftf1  48079  fargshiftfo  48080  ichnreuop  48110  ichreuopeq  48111  elsprel  48113  spr0nelg  48114  sprel  48122  prelspr  48124  sprsymrelf1lem  48129  sprsymrelfolem2  48131  paireqne  48149  prprelb  48154  prprelprb  48155  reupr  48160  reuopreuprim  48164  fmtnoprmfac1lem  48205  fmtnofac2  48210  m1expevenALTV  48301  odd2np1ALTV  48328  opoeALTV  48337  opeoALTV  48338  perfectALTVlem2  48376  isgbe  48405  isgbow  48406  isgbo  48407  sbgoldbalt  48435  sgoldbeven3prm  48437  mogoldbb  48439  nnsum3primesgbe  48446  nnsum3primesle9  48448  nnsum4primesodd  48450  nnsum4primesoddALTV  48451  vopnbgrel  48508  dfclnbgr6  48510  dfnbgr6  48511  isuspgrim0  48548  isuspgrimlem  48549  clnbgrgrim  48588  usgrgrtrirex  48604  stgredgel  48611  stgrusgra  48613  stgr1  48615  grlimgrtri  48657  gpgiedgdmel  48703  gpgedgel  48704  gpgprismgr4cycllem10  48758  pgnbgreunbgrlem1  48767  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  pgnbgreunbgrlem4  48773  pgnbgreunbgr  48779  uspgrsprf1  48801  uspgrsprfo  48802  0nodd  48824  1odd  48825  2nodd  48826  0even  48891  1neven  48892  2even  48893  2zlidl  48894  2zrngamgm  48899  2zrngagrp  48903  2zrngmmgm  48906  2zrngnmrid  48910  suppmptcfin  49041  lcoval  49077  linc0scn0  49088  linc1  49090  el0ldep  49131  snlindsntor  49136  blenval  49236  nn0sumshdiglemB  49285  itcoval1  49328  mo0  49477  eloprab1st2nd  49531  oppcmndclem  49680  sectpropdlem  49699  invpropdlem  49701  isopropdlem  49703  upciclem1  49829  oppcup3lem  49869  isthincd2lem1  50088  termcbasmo  50146  isinito2lem  50161  arweuthinc  50192  arweutermc  50193  discsntermlem  50233  basrestermcfolem  50234