Theorem eqeq1 2766

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  eqeq1i  2767  eqtr  2782  eqtr2  2783  iseqsetvlem  2825  eqsb1  2888  cbvexeqsetf  3469  rexraleqim  3606  eqvincf  3609  pm13.183  3625  moeq  3670  mob  3680  euind  3687  reu2eqd  3699  reuind  3716  eqsbc1  3790  sbceqal  3805  csbhypf  3880  uniiunlem  4040  snjust  4581  elsng  4596  elprg  4605  reusngf  4633  rexreusng  4638  reuprg0  4661  rabrsn  4683  preq12bg  4811  intab  4936  uniintsn  4943  dfiun2g  4987  dfiin2g  4988  disji2  5084  disjprg  5096  unopab  5180  eusv1  5348  reusv2lem2  5356  reusv3  5362  axprg  5394  opthg  5445  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  propeqop  5476  euotd  5482  otiunsndisj  5489  elopabw  5496  solin  5582  elxpi  5669  opbrop  5745  relop  5822  ideqg  5823  dmopab2rex  5893  elrnmpt  5934  elrnmpt1  5936  elrnmptg  5937  restidsing  6042  somin1  6120  cnveqb  6183  reu3op  6279  reuop  6280  ordequn  6451  iotaval2  6492  funopg  6555  f0rn0  6749  fvelrnb  6927  fvmptg  6973  fndmin  7026  eldmrexrn  7072  foelrn  7088  foelrnf  7089  foco2  7090  fmptco  7111  funopsn  7130  funopsnOLD  7131  funsndifnop  7134  fmptsng  7152  fmptsnd  7153  tpres  7185  eufnfv  7213  elabrex  7226  elabrexg  7227  abrexco  7228  f1veqaeq  7240  fpropnf1  7251  nf1const  7288  isosolem  7331  f1oiso  7335  eusvobj2  7388  oprabidw  7427  oprabid  7428  f1opr  7452  oprabv  7456  0mpo0  7479  elrnmpog  7531  elrnmpo  7532  elrnmpores  7534  ralrnmpo  7535  ov3  7559  ov6g  7560  ovelrn  7572  caovcang  7597  caovcan  7600  caofidlcan  7698  uniuni  7745  orduninsuc  7823  funcnvuni  7913  fiunlem  7923  fiun  7924  f1iun  7925  f1oweALT  7953  opiota  8040  eloprabi  8044  mpof1o2d  8105  frxp  8106  funsssuppss  8170  dftpos4  8225  tz7.44-2  8378  tz7.44-3  8379  oev  8483  oalimcl  8529  omlimcl  8547  odi  8548  omeu  8554  oeeui  8572  nneob  8626  omopth  8632  eldifsucnn  8634  elqsg  8745  qsdisj  8776  qsel  8778  brecop  8792  eroveu  8794  erovlem  8795  elixpsn  8919  ixpsnf1o  8920  boxcutc  8923  2dom  9011  fundmen  9012  xpf1o  9111  nneneq  9174  fofinf1o  9275  elfi  9359  elfiun  9376  dffi3  9377  brwdom  9515  brwdom3  9530  unwdomg  9532  xpwdomg  9533  noinfep  9615  cantnfp1lem1  9633  cantnfp1lem3  9635  cantnflem1  9644  ssttrcl  9670  ttrclselem2  9681  scott0  9844  updjudhcoinrg  9891  updjud  9892  carden2a  9924  cardiun  9940  pm54.43lem  9958  alephval3  10066  dfac5lem3  10081  dfac5lem4  10082  dfac5lem4OLD  10084  dfac2b  10087  kmlem9  10115  kmlem12  10118  cardcf  10208  cfeq0  10213  cfsuc  10214  cff1  10215  cflim2  10220  cfss  10222  isfin5  10256  fin1a2lem11  10367  fin1a2lem13  10369  brdom7disj  10488  brdom6disj  10489  canthp1lem2  10611  canthp1  10612  tskuni  10741  gruina  10776  genpv  10957  genpelv  10958  addsrmo  11031  mulsrmo  11032  ltsosr  11052  ltresr  11098  axcnre  11122  axpre-lttri  11123  ltordlem  11712  ltord1  11713  fimaxre3  12138  supaddc  12159  supadd  12160  supmul1  12161  supmullem1  12162  supmullem2  12163  supmul  12164  creur  12189  creui  12190  nn1m1nn  12231  elz  12570  nn0ind-raph  12673  xnegeq  13210  xmullem2  13268  xmulasslem  13288  fleqceilz  13864  fseqsupubi  13991  sqeqor  14229  nn0opth2  14285  hash1snb  14432  hash2prde  14483  prprrab  14486  hash2pwpr  14489  tpf1ofv1  14510  tpf1ofv2  14511  tpfo  14513  fi1uzind  14520  wrd2ind  14736  cshfn  14803  cshf1  14823  2cshwcshw  14838  scshwfzeqfzo  14839  pfx2  14960  s3iunsndisj  14981  relexpsucnnr  15038  relexprelg  15051  rtrclreclem3  15073  shftfval  15083  sgnval  15101  sgn3da  15114  sgn0bi  15116  sgnnbi  15117  sgnpbi  15118  sgnmul  15120  01sqrexlem6  15274  reusq0  15492  summo  15744  fsum  15747  telfsumo  15830  infcvgaux1i  15887  infcvgaux2i  15888  mertenslem1  15914  mertenslem2  15915  mertens  15916  prodmo  15966  fprod  15971  ruclem12  16273  mod2eq1n2dvds  16381  divalg  16437  ndvdssub  16443  sadcp1  16489  smupp1  16514  gcdval  16530  bezoutlem1  16573  bezoutlem3  16575  bezoutlem4  16576  bezout  16577  lcmval  16626  coprmgcdb  16683  coprmdvds1  16686  divgcdcoprmex  16700  dvdsprime  16721  nprm  16722  dvdsprm  16738  coprm  16746  qnumval  16772  qdenval  16773  m1dvdsndvds  16834  reumodprminv  16840  pcval  16880  pceu  16882  pczpre  16883  pcdiv  16888  4sqlem2  16985  4sqlem4  16988  4sqlem12  16992  4sq  17000  vdwapval  17009  vdwapun  17010  vdwlem6  17022  cshwrepswhash1  17138  acsfn  17691  initoid  18034  termoid  18035  cat1lem  18129  posi  18349  gsumval2a  18719  smndex2dnrinv  18952  mgm2nsgrplem2  18956  mgm2nsgrplem3  18957  sgrp2nmndlem5  18966  mgmnsgrpex  18968  sgrpnmndex  18969  cyccom  19244  ghmf1  19286  conjnmzb  19293  orbsta  19353  symgextfv  19458  symgextfo  19462  symgfixfo  19479  pmtrprfval  19527  pmtrprfvalrn  19528  psgneu  19546  psgnval  19547  psgnvali  19548  psgnvalii  19549  odfval  19572  odval  19574  dfod2  19604  submod  19609  isslw  19648  sylow2alem1  19657  sylow3lem2  19668  lsmelvalm  19691  lsmdisj2  19722  efgrelexlemb  19790  frgpup3lem  19817  cyggeninv  19923  gsumval3eu  19944  gsumval3lem2  19946  gsummpt1n0  20005  nn0gsumfz  20024  dprddisj2  20081  dpjrid  20104  pgpfac1lem3  20119  rrgeq0i  20749  domneq0  20758  domnlcanb  20770  domnrcanb  20772  abveq0  20867  abvtrivd  20881  lss1d  21030  lspsn  21069  ellspsn  21070  lspprel  21161  prmirredlem  21524  znf1o  21603  znfld  21612  znunit  21615  cygznlem3  21621  psgndif  21654  ipeq0  21690  obsip  21773  frlmphl  21833  uvcvval  21838  ellspd  21854  psrlidm  22013  psrridm  22014  psrascl  22030  mvrval2  22034  mvrf1  22037  mplmonmul  22089  evlslem3  22133  selvvvval  22195  mhpsclcl  22212  psdmplcl  22227  psdmul  22231  psdmvr  22234  coe1tm  22336  coe1tmfv2  22338  cply1coe0  22364  cply1coe0bi  22365  gsummoncoe1  22371  mamufacex  22456  mat1comp  22500  mat1dimelbas  22531  mat1dimid  22534  scmatel  22565  scmateALT  22572  mavmulsolcl  22611  marrepeval  22623  marepveval  22628  mdetunilem8  22679  maducoeval2  22700  madugsum  22703  minmar1eval  22709  symgmatr01lem  22713  symgmatr01  22714  gsummatr01lem3  22717  gsummatr01lem4  22718  gsummatr01  22719  m2cpm  22801  m2cpminvid2lem  22814  decpmatid  22830  monmatcollpw  22839  pmatcollpw3fi1lem1  22846  mp2pm2mplem4  22869  fvmptnn04ifc  22912  chfacffsupp  22916  chfacfscmul0  22918  chfacfscmulgsum  22920  chfacfpmmul0  22922  chfacfpmmulgsum  22924  cpmadumatpoly  22943  cayleyhamilton  22950  cayleyhamiltonALT  22951  istopon  22972  toponsspwpw  22982  fctop  23064  cctop  23066  ppttop  23067  pptbas  23068  epttop  23069  t0sep  23384  t1sep2  23429  cmpsublem  23459  cmpsub  23460  unisngl  23587  txuni2  23625  elpt  23632  ptbasfi  23641  xkoopn  23649  ptpjopn  23672  ptclsg  23675  dfac14lem  23677  ptcnp  23682  ptrescn  23699  tx1stc  23710  qtopeu  23776  kqt0lem  23796  isr0  23797  hauspwpwf1  24047  xmeteq0  24398  imasf1oxmet  24435  comet  24573  stdbdxmet  24575  met2ndci  24582  prdsxmslem2  24589  nrmmetd  24634  tngngp  24714  tngngp3  24716  xrsxmet  24870  iccpnfcnv  25006  iccpnfhmeo  25007  cnheibor  25017  elovolm  25537  ovolgelb  25542  ovolicc1  25578  ovolicc  25585  ioorval  25636  uniioombllem6  25650  dyadmax  25660  dyadmbl  25662  i1fadd  25757  i1fmul  25758  itg1addlem3  25760  i1fmulc  25765  itg2l  25791  itg2leub  25796  limcmpt  25945  limcco  25955  dvcobr  26008  deg1ldg  26152  ig1pval  26236  elply  26255  elply2  26256  coeval  26283  coe1termlem  26318  coe1term  26319  plyn0mulidp  26345  quotval  26356  plydivlem4  26360  plydivex  26361  vieta1  26376  aannenlem2  26393  aalioulem2  26397  abelthlem9  26503  logtayllem  26724  logtayl  26725  isosctrlem2  26884  leibpilem2  27006  rlimcnp2  27031  efrlim  27034  mpodvdsmulf1o  27258  dvdsmulf1o  27260  perfectlem2  27294  lgsfval  27366  lgsval2lem  27371  lgsqrmodndvds  27417  lgsdchrval  27418  gausslemma2dlem0i  27428  2lgslem1b  27456  2lgslem3  27468  2sqlem2  27482  2sqlem8  27490  2sqlem9  27491  2sqlem11  27493  addsq2reu  27504  dchrisum0flblem1  27572  padicval  27681  padicabv  27694  ostth1  27697  ltsval2  27720  ltsintdifex  27725  ltsres  27726  nolt02o  27759  madef  27929  addsval2  28056  addsproplem2  28063  addsproplem4  28065  addsproplem5  28066  addsproplem6  28067  addsprop  28069  addcuts  28071  leadds1  28082  addsuniflem  28094  addsunif  28095  addsasslem1  28096  addsasslem2  28097  addbdaylem  28110  negsprop  28128  negsid  28134  mulsval2lem  28203  mulsproplem9  28217  mulsproplem12  28220  mulsprop  28223  sltmuls1  28240  sltmuls2  28241  mulsuniflem  28242  addsdilem1  28244  addsdilem2  28245  mulsasslem1  28256  mulsasslem2  28257  mulsunif2  28263  precsexlemcbv  28299  precsexlem9  28308  precsexlem11  28310  n0s0suc  28435  onsfi  28449  n0s0m1  28455  nn1m1nns  28467  eucliddivs  28469  n0seo  28514  zseo  28515  expsval  28518  bdayfinbndcbv  28559  bdayfinbndlem1  28560  bdayfinbndlem2  28561  bdayfinbnd  28562  elz12s  28565  z12zsodd  28575  z12sge0  28576  recut  28587  elreno2  28588  renegscl  28591  readdscl  28592  remulscllem1  28593  remulscl  28595  axtgcgrid  28632  axtgbtwnid  28635  islmib  28960  inaghl  29039  axpaschlem  29141  axlowdimlem15  29157  axlowdim  29162  upgredg2vtx  29342  edglnl  29344  umgredgnlp  29348  usgredg2vtxeuALT  29423  uspgredg2v  29425  ushgredgedgloop  29432  nbusgredgeu  29567  cusgrfilem2  29657  cusgrfi  29659  vtxdushgrfvedg  29691  1loopgrvd2  29704  rusgr1vtxlem  29788  wlkeq  29834  wlkp1lem8  29879  upgrwlkdvdelem  29936  crctcshwlkn0lem6  30015  wlknwwlksnbij  30088  rusgrnumwwlkl1  30171  clwlkclwwlklem2a1  30194  clwwlknscsh  30264  eleclclwwlkn  30278  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  clwwlknon1sn  30302  frgr3vlem1  30475  3vfriswmgrlem  30479  frgrncvvdeqlem3  30503  wlkl0  30569  frgrreggt1  30595  nvz  30872  nmosetn0  30968  nmoolb  30974  nmoubi  30975  nmlno0lem  30996  nmlno0i  30997  hvsubeq0  31271  hvaddcan  31273  normsub0  31339  norm1exi  31453  pjhval  31600  omlsii  31606  omlsi  31607  pjoml  31639  h1de2ci  31759  spansneleq  31773  h1datomi  31784  h1datom  31785  spansncv  31856  5oalem6  31862  pj11  31917  nmopsetn0  32068  nmfnsetn0  32081  nmoplb  32110  nmopub  32111  nmfnlb  32127  nmfnleub  32128  nmlnop0iALT  32198  nmlnop0  32201  lnopeq  32212  nmopun  32217  nmcexi  32229  branmfn  32308  pjnmopi  32351  pj3i  32411  atss  32549  atom1d  32556  chirred  32598  cdj3lem2  32638  eqelbid  32674  elabreximd  32709  disjxpin  32788  disjunsn  32794  br8d  32810  fmptcof2  32859  psgnfzto1stlem  33280  sgnsval  33341  elrgspnlem2  33424  elrgspnlem3  33425  domnlcanOLD  33464  linds2eq  33567  elrspunsn  33615  mxidlmax  33653  1arithidomlem1  33731  1arithidom  33733  1arithufdlem1  33740  1arithufdlem2  33741  1arithufdlem3  33742  1arithufdlem4  33743  1arithufd  33744  dfufd2  33746  ply1dg1rt  33776  selvply1rhmlem2  33818  mplvrpmrhm  33844  psrmonmul  33847  esplyfvaln  33871  lbsdiflsp0  33923  fedgmullem1  33926  fedgmullem2  33927  rtelextdg2lem  34023  constrsuc  34035  constrcbvlem  34052  2sqr3minply  34077  madjusmdetlem2  34125  madjusmdet  34128  zarclssn  34170  xrge0iifcnv  34230  xrge0iifcv  34231  xrge0iifhom  34234  xrge0tmd  34242  xrge0tmdALT  34243  esumc  34348  signspval  34846  tgoldbachgt  34957  bnj1468  35141  fineqvnttrclselem3  35419  fineqvnttrclse  35420  f1resfz0f1d  35464  acycgrcycl  35497  sconnpi1  35589  cvmlift3lem2  35670  satfv0  35708  satfv1  35713  satfbrsuc  35716  satfrnmapom  35720  satfv0fun  35721  satf0op  35727  sat1el2xp  35729  fmlafvel  35735  fmla1  35737  isfmlasuc  35738  fmlaomn0  35740  gonan0  35742  goaln0  35743  gonar  35745  goalr  35747  fmla0disjsuc  35748  fmlasucdisj  35749  satffunlem1lem1  35752  satffunlem2lem1  35754  dmopab3rexdif  35755  satfv0fvfmla0  35763  sategoelfvb  35769  ex-sategoelel  35771  satfv1fvfmla1  35773  2goelgoanfmla1  35774  ex-sategoelelomsuc  35776  ex-sategoelel12  35777  prv1n  35781  ellcsrspsn  35991  r1peuqusdeg1  35993  br8  36106  br6  36107  br4  36108  rdgprc0  36141  dfrdg2  36143  dfbigcup2  36247  elsingles  36266  dfiota3  36271  brimageg  36275  brdomaing  36283  brrangeg  36284  dfrdg4  36301  elaltxp  36325  funtransport  36381  fvtransport  36382  brsegle  36458  funray  36490  fvray  36491  funline  36492  fvline  36494  ellines  36502  linethru  36503  rankeq1o  36521  subtr  36674  subtr2  36675  nn0prpw  36683  bj-elabd2ALT  37410  bj-gabss  37420  bj-imafv  37743  topdifinffinlem  37841  topdifinffin  37842  topdifinfeq  37844  finxpreclem2  37884  finxpreclem3  37887  fvineqsnf1  37904  fvineqsneu  37905  wl-ax12v2cl  38000  wl-dfclel  38009  wl-issetft  38085  fin2so  38106  ptrest  38118  poimirlem25  38144  poimirlem26  38145  poimirlem27  38146  poimirlem28  38147  poimirlem31  38150  poimirlem32  38151  heicant  38154  mblfinlem2  38157  mblfinlem3  38158  mblfinlem4  38159  ismblfin  38160  itg2addnclem  38170  itg2addnclem3  38172  itg2addnc  38173  ftc1anc  38200  unirep  38213  sdclem2  38241  sdclem1  38242  sdc  38243  fdc  38244  isbnd  38279  heibor1lem  38308  heiborlem4  38313  heiborlem6  38315  heiborlem10  38319  ismgmOLD  38349  maxidlmax  38542  prnc  38566  isfldidl  38567  dmnnzd  38574  disjressuc2  38910  qsdisjALTV  39198  eqvrelqsel  39199  riotasvd  39580  lshpdisj  39611  lsat0cv  39657  lcvexchlem4  39661  lcvexchlem5  39662  lshpkrlem1  39734  lshpkrlem2  39735  lshpkrlem3  39736  lshpkrcl  39740  islshpkrN  39744  atnle  39941  glbconxN  40002  isline  40363  ispointN  40366  pmapglbx  40393  ispsubcl2N  40571  lhp2atnle  40657  cdleme43fsv1snlem  41044  cdleme40v  41093  cdlemkid5  41559  cdlemkid  41560  dvhb1dimN  41610  dib1dim  41789  dicopelval  41801  dicelval1sta  41811  diclspsn  41818  dihvalcqpre  41859  dihglblem2aN  41917  dihglblem2N  41918  dih1dimatlem  41953  dihpN  41960  dochfl1  42100  lcfl7N  42125  lcf1o  42175  hvmapvalvalN  42385  hdmapval2lem  42455  aks6d1c1  42733  aks6d1c4  42741  sticksstones10  42772  sticksstones12a  42774  aks6d1c7  42801  sn-iotalem  42840  fiabv  43154  evlsbagval  43168  fsuppind  43172  absnw  43260  elrfi  43275  nacsfg  43286  mzpcompact2lem  43332  eldioph2b  43344  eldioph3  43347  eldiophss  43355  diophrex  43356  elnn0rabdioph  43380  rencldnfilem  43397  elpell1qr  43424  elpell14qr  43426  elpell1234qr  43428  jm2.27  43585  rmydioph  43591  expdiophlem2  43599  wepwsolem  43619  aomclem6  43636  lnr2i  43693  lpirlnr  43694  hbtlem2  43701  hbtlem4  43703  hbtlem5  43705  rngunsnply  43746  flcidc  43747  onsucelab  43840  limnsuc  43842  nnoeomeqom  43889  cantnfresb  43901  tfsconcatfv2  43917  tfsconcatb0  43921  oaun3lem1  43951  oadif1lem  43956  oadif1  43957  clcnvlem  44199  brtrclfv2  44303  frege55lem1c  44492  frege104  44543  clsk1indlem0  44617  clsk1indlem2  44618  clsk1indlem3  44619  clsk1indlem4  44620  clsk1indlem1  44621  pm13.192  44986  equncomVD  45443  csbingVD  45459  csbsngVD  45468  csbfv12gALTVD  45474  relopabVD  45476  refsum2cnlem1  45617  elrnmptf  45759  upbdrech  45884  ssfiunibd  45888  iccshift  46094  iooshift  46098  fsumf1of  46150  limcperiod  46204  climinf2mpt  46288  climinfmpt  46289  cncfshiftioo  46466  itgiccshift  46554  itgperiod  46555  stoweidlem46  46620  fourierdlem29  46710  fourierdlem37  46718  fourierdlem48  46728  fourierdlem51  46731  fourierdlem54  46734  fourierdlem62  46742  fourierdlem79  46759  fourierdlem81  46761  fourierdlem82  46762  fourierdlem92  46772  fourierdlem96  46776  fourierdlem97  46777  fourierdlem98  46778  fourierdlem99  46779  fourierdlem103  46783  fourierdlem104  46784  fourierdlem105  46785  fourierdlem108  46788  fourierdlem110  46790  fourierdlem112  46792  etransclem1  46809  etransclem5  46813  etransclem17  46825  etransclem32  46840  etransclem41  46849  sge0f1o  46956  sge0resplit  46980  sge0fodjrnlem  46990  nnfoctbdjlem  47029  nnfoctbdj  47030  ovnval  47115  ovnlecvr  47132  ovnpnfelsup  47133  ovn0lem  47139  hoidmvval  47151  hoidmvlelem1  47169  ovnhoilem1  47175  ovnhoi  47177  ovnlecvr2  47184  hoidifhspval3  47193  hspmbllem2  47201  hoimbl  47205  ovnsubadd2  47220  ovolval5lem2  47227  ovolval5lem3  47228  ovolval5  47229  ovnovol  47233  sinnpoly  47485  fsetsnf  47645  fsetsnfo  47647  fcoresf1  47663  aiotaval  47689  euoreqb  47703  afv0fv0  47743  afvfv0bi  47746  afvelrnb  47757  afvelrnb0  47758  afv20defat  47826  otiunsndisjX  47873  fun2dmnopgexmpl  47878  2ffzoeq  47922  modmkpkne  47961  elsetpreimafvb  47990  imasetpreimafvbijlemfo  48011  fargshiftf1  48047  fargshiftfo  48048  ichnreuop  48078  ichreuopeq  48079  elsprel  48081  spr0nelg  48082  sprel  48090  prelspr  48092  sprsymrelf1lem  48097  sprsymrelfolem2  48099  paireqne  48117  prprelb  48122  prprelprb  48123  reupr  48128  reuopreuprim  48132  fmtnoprmfac1lem  48173  fmtnofac2  48178  m1expevenALTV  48269  odd2np1ALTV  48296  opoeALTV  48305  opeoALTV  48306  perfectALTVlem2  48344  isgbe  48373  isgbow  48374  isgbo  48375  sbgoldbalt  48403  sgoldbeven3prm  48405  mogoldbb  48407  nnsum3primesgbe  48414  nnsum3primesle9  48416  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  vopnbgrel  48476  dfclnbgr6  48478  dfnbgr6  48479  isuspgrim0  48516  isuspgrimlem  48517  clnbgrgrim  48556  usgrgrtrirex  48572  stgredgel  48579  stgrusgra  48581  stgr1  48583  grlimgrtri  48625  gpgiedgdmel  48671  gpgedgel  48672  gpgprismgr4cycllem10  48726  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem4  48741  pgnbgreunbgr  48747  uspgrsprf1  48769  uspgrsprfo  48770  0nodd  48792  1odd  48793  2nodd  48794  0even  48859  1neven  48860  2even  48861  2zlidl  48862  2zrngamgm  48867  2zrngagrp  48871  2zrngmmgm  48874  2zrngnmrid  48878  suppmptcfin  48998  lcoval  49034  linc0scn0  49045  linc1  49047  el0ldep  49088  snlindsntor  49093  blenval  49193  nn0sumshdiglemB  49242  itcoval1  49285  mo0  49435  eloprab1st2nd  49489  oppcmndclem  49638  sectpropdlem  49657  invpropdlem  49659  isopropdlem  49661  upciclem1  49787  oppcup3lem  49827  isthincd2lem1  50046  termcbasmo  50104  isinito2lem  50119  arweuthinc  50150  arweutermc  50151  discsntermlem  50191  basrestermcfolem  50192