Theorem eqeq1 2740

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqeq1i  2741  eqtr  2756  eqtr2  2757  iseqsetvlem  2799  eqsb1  2862  cbvexeqsetf  3444  rexraleqim  3589  eqvincf  3592  pm13.183  3608  moeq  3653  mob  3663  euind  3670  reu2eqd  3682  reuind  3699  eqsbc1  3775  sbceqal  3790  csbhypf  3865  uniiunlem  4027  snjust  4566  elsng  4581  elprg  4590  reusngf  4618  rexreusng  4623  reuprg0  4646  rabrsn  4668  preq12bg  4796  intab  4920  uniintsn  4927  dfiun2g  4972  dfiin2g  4973  disji2  5069  disjprg  5081  unopab  5165  eusv1  5333  reusv2lem2  5341  reusv3  5347  axprg  5379  opthg  5430  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  propeqop  5461  euotd  5467  otiunsndisj  5474  elopabw  5481  solin  5566  elxpi  5653  opbrop  5729  relop  5805  ideqg  5806  dmopab2rex  5872  elrnmpt  5913  elrnmpt1  5915  elrnmptg  5916  restidsing  6018  somin1  6096  cnveqb  6160  reu3op  6256  reuop  6257  ordequn  6428  iotaval2  6469  funopg  6532  f0rn0  6725  fvelrnb  6900  fvmptg  6945  fndmin  6997  eldmrexrn  7043  foelrn  7059  foelrnf  7060  foco2  7061  fmptco  7082  funopsn  7101  funopsnOLD  7102  funsndifnop  7105  fmptsng  7123  fmptsnd  7124  tpres  7156  eufnfv  7184  elabrex  7197  elabrexg  7198  abrexco  7199  f1veqaeq  7211  fpropnf1  7222  nf1const  7259  isosolem  7302  f1oiso  7306  eusvobj2  7359  oprabidw  7398  oprabid  7399  f1opr  7423  oprabv  7427  0mpo0  7450  elrnmpog  7502  elrnmpo  7503  elrnmpores  7505  ralrnmpo  7506  ov3  7530  ov6g  7531  ovelrn  7543  caovcang  7568  caovcan  7571  caofidlcan  7669  uniuni  7716  orduninsuc  7794  funcnvuni  7883  fiunlem  7895  fiun  7896  f1iun  7897  f1oweALT  7925  opiota  8012  eloprabi  8016  frxp  8076  funsssuppss  8140  dftpos4  8195  tz7.44-2  8346  tz7.44-3  8347  oev  8449  oalimcl  8495  omlimcl  8513  odi  8514  omeu  8520  oeeui  8538  nneob  8592  omopth  8598  eldifsucnn  8600  elqsg  8710  qsdisj  8741  qsel  8743  brecop  8757  eroveu  8759  erovlem  8760  elixpsn  8885  ixpsnf1o  8886  boxcutc  8889  2dom  8977  fundmen  8978  xpf1o  9077  nneneq  9140  fofinf1o  9242  elfi  9326  elfiun  9343  dffi3  9344  brwdom  9482  brwdom3  9497  unwdomg  9499  xpwdomg  9500  noinfep  9581  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnflem1  9610  ssttrcl  9636  ttrclselem2  9647  scott0  9810  updjudhcoinrg  9857  updjud  9858  carden2a  9890  cardiun  9906  pm54.43lem  9924  alephval3  10032  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2b  10053  kmlem9  10081  kmlem12  10084  cardcf  10174  cfeq0  10178  cfsuc  10179  cff1  10180  cflim2  10185  cfss  10187  isfin5  10221  fin1a2lem11  10332  fin1a2lem13  10334  brdom7disj  10453  brdom6disj  10454  canthp1lem2  10576  canthp1  10577  tskuni  10706  gruina  10741  genpv  10922  genpelv  10923  addsrmo  10996  mulsrmo  10997  ltsosr  11017  ltresr  11063  axcnre  11087  axpre-lttri  11088  ltordlem  11675  ltord1  11676  fimaxre3  12102  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmullem2  12127  supmul  12128  creur  12153  creui  12154  nn1m1nn  12195  elz  12526  nn0ind-raph  12629  xnegeq  13159  xmullem2  13217  xmulasslem  13237  fleqceilz  13813  fseqsupubi  13940  sqeqor  14178  nn0opth2  14234  hash1snb  14381  hash2prde  14432  prprrab  14435  hash2pwpr  14438  tpf1ofv1  14459  tpf1ofv2  14460  tpfo  14462  fi1uzind  14469  wrd2ind  14685  cshfn  14752  cshf1  14772  2cshwcshw  14787  scshwfzeqfzo  14788  pfx2  14909  s3iunsndisj  14930  relexpsucnnr  14987  relexprelg  15000  rtrclreclem3  15022  shftfval  15032  sgnval  15050  01sqrexlem6  15209  reusq0  15427  summo  15679  fsum  15682  telfsumo  15765  infcvgaux1i  15822  infcvgaux2i  15823  mertenslem1  15849  mertenslem2  15850  mertens  15851  prodmo  15901  fprod  15906  ruclem12  16208  mod2eq1n2dvds  16316  divalg  16372  ndvdssub  16378  sadcp1  16424  smupp1  16449  gcdval  16465  bezoutlem1  16508  bezoutlem3  16510  bezoutlem4  16511  bezout  16512  lcmval  16561  coprmgcdb  16618  coprmdvds1  16621  divgcdcoprmex  16635  dvdsprime  16656  nprm  16657  dvdsprm  16673  coprm  16681  qnumval  16707  qdenval  16708  m1dvdsndvds  16769  reumodprminv  16775  pcval  16815  pceu  16817  pczpre  16818  pcdiv  16823  4sqlem2  16920  4sqlem4  16923  4sqlem12  16927  4sq  16935  vdwapval  16944  vdwapun  16945  vdwlem6  16957  cshwrepswhash1  17073  acsfn  17625  initoid  17968  termoid  17969  cat1lem  18063  posi  18283  gsumval2a  18653  smndex2dnrinv  18886  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem5  18900  mgmnsgrpex  18902  sgrpnmndex  18903  cyccom  19178  ghmf1  19221  conjnmzb  19228  orbsta  19288  symgextfv  19393  symgextfo  19397  symgfixfo  19414  pmtrprfval  19462  pmtrprfvalrn  19463  psgneu  19481  psgnval  19482  psgnvali  19483  psgnvalii  19484  odfval  19507  odval  19509  dfod2  19539  submod  19544  isslw  19583  sylow2alem1  19592  sylow3lem2  19603  lsmelvalm  19626  lsmdisj2  19657  efgrelexlemb  19725  frgpup3lem  19752  cyggeninv  19858  gsumval3eu  19879  gsumval3lem2  19881  gsummpt1n0  19940  nn0gsumfz  19959  dprddisj2  20016  dpjrid  20039  pgpfac1lem3  20054  rrgeq0i  20676  domneq0  20685  domnlcanb  20697  domnrcanb  20699  abveq0  20795  abvtrivd  20809  lss1d  20958  lspsn  20997  ellspsn  20998  lspprel  21089  prmirredlem  21452  znf1o  21531  znfld  21540  znunit  21543  cygznlem3  21549  psgndif  21582  ipeq0  21618  obsip  21701  frlmphl  21761  uvcvval  21766  ellspd  21782  psrlidm  21940  psrridm  21941  psrascl  21957  mvrval2  21961  mvrf1  21964  mplmonmul  22014  evlslem3  22058  mhpsclcl  22113  psdmplcl  22128  psdmul  22132  psdmvr  22135  coe1tm  22238  coe1tmfv2  22240  cply1coe0  22266  cply1coe0bi  22267  gsummoncoe1  22273  mamufacex  22361  mat1comp  22405  mat1dimelbas  22436  mat1dimid  22439  scmatel  22470  scmateALT  22477  mavmulsolcl  22516  marrepeval  22528  marepveval  22533  mdetunilem8  22584  maducoeval2  22605  madugsum  22608  minmar1eval  22614  symgmatr01lem  22618  symgmatr01  22619  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  m2cpm  22706  m2cpminvid2lem  22719  decpmatid  22735  monmatcollpw  22744  pmatcollpw3fi1lem1  22751  mp2pm2mplem4  22774  fvmptnn04ifc  22817  chfacffsupp  22821  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  cpmadumatpoly  22848  cayleyhamilton  22855  cayleyhamiltonALT  22856  istopon  22877  toponsspwpw  22887  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  epttop  22974  t0sep  23289  t1sep2  23334  cmpsublem  23364  cmpsub  23365  unisngl  23492  txuni2  23530  elpt  23537  ptbasfi  23546  xkoopn  23554  ptpjopn  23577  ptclsg  23580  dfac14lem  23582  ptcnp  23587  ptrescn  23604  tx1stc  23615  qtopeu  23681  kqt0lem  23701  isr0  23702  hauspwpwf1  23952  xmeteq0  24303  imasf1oxmet  24340  comet  24478  stdbdxmet  24480  met2ndci  24487  prdsxmslem2  24494  nrmmetd  24539  tngngp  24619  tngngp3  24621  xrsxmet  24775  iccpnfcnv  24911  iccpnfhmeo  24912  cnheibor  24922  elovolm  25442  ovolgelb  25447  ovolicc1  25483  ovolicc  25490  ioorval  25541  uniioombllem6  25555  dyadmax  25565  dyadmbl  25567  i1fadd  25662  i1fmul  25663  itg1addlem3  25665  i1fmulc  25670  itg2l  25696  itg2leub  25701  limcmpt  25850  limcco  25860  dvcobr  25913  deg1ldg  26057  ig1pval  26141  elply  26160  elply2  26161  coeval  26188  coe1termlem  26223  coe1term  26224  quotval  26258  plydivlem4  26262  plydivex  26263  vieta1  26278  aannenlem2  26295  aalioulem2  26299  abelthlem9  26405  logtayllem  26623  logtayl  26624  isosctrlem2  26783  leibpilem2  26905  rlimcnp2  26930  efrlim  26933  mpodvdsmulf1o  27157  dvdsmulf1o  27159  perfectlem2  27193  lgsfval  27265  lgsval2lem  27270  lgsqrmodndvds  27316  lgsdchrval  27317  gausslemma2dlem0i  27327  2lgslem1b  27355  2lgslem3  27367  2sqlem2  27381  2sqlem8  27389  2sqlem9  27390  2sqlem11  27392  addsq2reu  27403  dchrisum0flblem1  27471  padicval  27580  padicabv  27593  ostth1  27596  ltsval2  27620  ltsintdifex  27625  ltsres  27626  nolt02o  27659  madef  27828  addsval2  27955  addsproplem2  27962  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  addsprop  27968  addcuts  27970  leadds1  27981  addsuniflem  27993  addsunif  27994  addsasslem1  27995  addsasslem2  27996  addbdaylem  28009  negsprop  28027  negsid  28033  mulsval2lem  28102  mulsproplem9  28116  mulsproplem12  28119  mulsprop  28122  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  mulsunif2  28162  precsexlemcbv  28198  precsexlem9  28207  precsexlem11  28209  n0s0suc  28334  onsfi  28348  n0s0m1  28354  nn1m1nns  28366  eucliddivs  28368  n0seo  28413  zseo  28414  expsval  28417  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  bdayfinbnd  28461  elz12s  28464  z12zsodd  28474  z12sge0  28475  recut  28486  elreno2  28487  renegscl  28490  readdscl  28491  remulscllem1  28492  remulscl  28494  axtgcgrid  28531  axtgbtwnid  28534  islmib  28855  inaghl  28913  axpaschlem  29009  axlowdimlem15  29025  axlowdim  29030  upgredg2vtx  29210  edglnl  29212  umgredgnlp  29216  usgredg2vtxeuALT  29291  uspgredg2v  29293  ushgredgedgloop  29300  nbusgredgeu  29435  cusgrfilem2  29525  cusgrfi  29527  vtxdushgrfvedg  29559  1loopgrvd2  29572  rusgr1vtxlem  29656  wlkeq  29702  wlkp1lem8  29747  upgrwlkdvdelem  29804  crctcshwlkn0lem6  29883  wlknwwlksnbij  29956  rusgrnumwwlkl1  30039  clwlkclwwlklem2a1  30062  clwwlknscsh  30132  eleclclwwlkn  30146  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwwlknon1sn  30170  frgr3vlem1  30343  3vfriswmgrlem  30347  frgrncvvdeqlem3  30371  wlkl0  30437  frgrreggt1  30463  nvz  30740  nmosetn0  30836  nmoolb  30842  nmoubi  30843  nmlno0lem  30864  nmlno0i  30865  hvsubeq0  31139  hvaddcan  31141  normsub0  31207  norm1exi  31321  pjhval  31468  omlsii  31474  omlsi  31475  pjoml  31507  h1de2ci  31627  spansneleq  31641  h1datomi  31652  h1datom  31653  spansncv  31724  5oalem6  31730  pj11  31785  nmopsetn0  31936  nmfnsetn0  31949  nmoplb  31978  nmopub  31979  nmfnlb  31995  nmfnleub  31996  nmlnop0iALT  32066  nmlnop0  32069  lnopeq  32080  nmopun  32085  nmcexi  32097  branmfn  32176  pjnmopi  32219  pj3i  32279  atss  32417  atom1d  32424  chirred  32466  cdj3lem2  32506  eqelbid  32544  elabreximd  32580  disjxpin  32658  disjunsn  32664  br8d  32681  fmptcof2  32730  sgn3da  32907  sgnmul  32908  sgnnbi  32911  sgnpbi  32912  sgn0bi  32913  psgnfzto1stlem  33161  sgnsval  33222  elrgspnlem2  33304  elrgspnlem3  33305  domnlcanOLD  33341  linds2eq  33441  elrspunsn  33489  mxidlmax  33525  1arithidomlem1  33595  1arithidom  33597  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  1arithufd  33608  dfufd2  33610  ply1dg1rt  33640  mplvrpmrhm  33691  psrmonmul  33694  esplyfvaln  33718  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  rtelextdg2lem  33870  constrsuc  33882  constrcbvlem  33899  2sqr3minply  33924  madjusmdetlem2  33972  madjusmdet  33975  zarclssn  34017  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iifhom  34081  xrge0tmd  34089  xrge0tmdALT  34090  esumc  34195  plymulx0  34691  signspval  34696  tgoldbachgt  34807  bnj1468  34988  fineqvnttrclselem3  35267  fineqvnttrclse  35268  f1resfz0f1d  35296  acycgrcycl  35329  sconnpi1  35421  cvmlift3lem2  35502  satfv0  35540  satfv1  35545  satfbrsuc  35548  satfrnmapom  35552  satfv0fun  35553  satf0op  35559  sat1el2xp  35561  fmlafvel  35567  fmla1  35569  isfmlasuc  35570  fmlaomn0  35572  gonan0  35574  goaln0  35575  gonar  35577  goalr  35579  fmla0disjsuc  35580  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem2lem1  35586  dmopab3rexdif  35587  satfv0fvfmla0  35595  sategoelfvb  35601  ex-sategoelel  35603  satfv1fvfmla1  35605  2goelgoanfmla1  35606  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  prv1n  35613  ellcsrspsn  35823  r1peuqusdeg1  35825  br8  35938  br6  35939  br4  35940  rdgprc0  35973  dfrdg2  35975  dfbigcup2  36079  elsingles  36098  dfiota3  36103  brimageg  36107  brdomaing  36115  brrangeg  36116  dfrdg4  36133  elaltxp  36157  funtransport  36213  fvtransport  36214  brsegle  36290  funray  36322  fvray  36323  funline  36324  fvline  36326  ellines  36334  linethru  36335  rankeq1o  36353  subtr  36496  subtr2  36497  nn0prpw  36505  bj-elabd2ALT  37232  bj-gabss  37242  bj-imafv  37565  topdifinffinlem  37663  topdifinffin  37664  topdifinfeq  37666  finxpreclem2  37706  finxpreclem3  37709  fvineqsnf1  37726  fvineqsneu  37727  wl-ax12v2cl  37822  wl-dfclel  37831  wl-issetft  37907  fin2so  37928  ptrest  37940  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anc  38022  unirep  38035  sdclem2  38063  sdclem1  38064  sdc  38065  fdc  38066  isbnd  38101  heibor1lem  38130  heiborlem4  38135  heiborlem6  38137  heiborlem10  38141  ismgmOLD  38171  maxidlmax  38364  prnc  38388  isfldidl  38389  dmnnzd  38396  disjressuc2  38732  qsdisjALTV  39020  eqvrelqsel  39021  riotasvd  39402  lshpdisj  39433  lsat0cv  39479  lcvexchlem4  39483  lcvexchlem5  39484  lshpkrlem1  39556  lshpkrlem2  39557  lshpkrlem3  39558  lshpkrcl  39562  islshpkrN  39566  atnle  39763  glbconxN  39824  isline  40185  ispointN  40188  pmapglbx  40215  ispsubcl2N  40393  lhp2atnle  40479  cdleme43fsv1snlem  40866  cdleme40v  40915  cdlemkid5  41381  cdlemkid  41382  dvhb1dimN  41432  dib1dim  41611  dicopelval  41623  dicelval1sta  41633  diclspsn  41640  dihvalcqpre  41681  dihglblem2aN  41739  dihglblem2N  41740  dih1dimatlem  41775  dihpN  41782  dochfl1  41922  lcfl7N  41947  lcf1o  41997  hvmapvalvalN  42207  hdmapval2lem  42277  aks6d1c1  42555  aks6d1c4  42563  sticksstones10  42594  sticksstones12a  42596  aks6d1c7  42623  sn-iotalem  42662  f1o2d2  42674  fiabv  42981  evlsbagval  43002  selvvvval  43018  fsuppind  43023  absnw  43111  elrfi  43126  nacsfg  43137  mzpcompact2lem  43183  eldioph2b  43195  eldioph3  43198  eldiophss  43206  diophrex  43207  elnn0rabdioph  43231  rencldnfilem  43248  elpell1qr  43275  elpell14qr  43277  elpell1234qr  43279  jm2.27  43436  rmydioph  43442  expdiophlem2  43450  wepwsolem  43470  aomclem6  43487  lnr2i  43544  lpirlnr  43545  hbtlem2  43552  hbtlem4  43554  hbtlem5  43556  rngunsnply  43597  flcidc  43598  onsucelab  43691  limnsuc  43693  nnoeomeqom  43740  cantnfresb  43752  tfsconcatfv2  43768  tfsconcatb0  43772  oaun3lem1  43802  oadif1lem  43807  oadif1  43808  clcnvlem  44050  brtrclfv2  44154  frege55lem1c  44343  frege104  44394  clsk1indlem0  44468  clsk1indlem2  44469  clsk1indlem3  44470  clsk1indlem4  44471  clsk1indlem1  44472  pm13.192  44837  equncomVD  45294  csbingVD  45310  csbsngVD  45319  csbfv12gALTVD  45325  relopabVD  45327  refsum2cnlem1  45468  elrnmptf  45611  upbdrech  45738  ssfiunibd  45742  iccshift  45948  iooshift  45952  fsumf1of  46004  limcperiod  46058  climinf2mpt  46142  climinfmpt  46143  cncfshiftioo  46320  itgiccshift  46408  itgperiod  46409  stoweidlem46  46474  fourierdlem29  46564  fourierdlem37  46572  fourierdlem48  46582  fourierdlem51  46585  fourierdlem54  46588  fourierdlem62  46596  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem92  46626  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem103  46637  fourierdlem104  46638  fourierdlem105  46639  fourierdlem108  46642  fourierdlem110  46644  fourierdlem112  46646  etransclem1  46663  etransclem5  46667  etransclem17  46679  etransclem32  46694  etransclem41  46703  sge0f1o  46810  sge0resplit  46834  sge0fodjrnlem  46844  nnfoctbdjlem  46883  nnfoctbdj  46884  ovnval  46969  ovnlecvr  46986  ovnpnfelsup  46987  ovn0lem  46993  hoidmvval  47005  hoidmvlelem1  47023  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  hoidifhspval3  47047  hspmbllem2  47055  hoimbl  47059  ovnsubadd2  47074  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovol  47087  sinnpoly  47339  fsetsnf  47499  fsetsnfo  47501  fcoresf1  47517  aiotaval  47543  euoreqb  47557  afv0fv0  47597  afvfv0bi  47600  afvelrnb  47611  afvelrnb0  47612  afv20defat  47680  otiunsndisjX  47727  fun2dmnopgexmpl  47732  2ffzoeq  47776  modmkpkne  47815  elsetpreimafvb  47844  imasetpreimafvbijlemfo  47865  fargshiftf1  47901  fargshiftfo  47902  ichnreuop  47932  ichreuopeq  47933  elsprel  47935  spr0nelg  47936  sprel  47944  prelspr  47946  sprsymrelf1lem  47951  sprsymrelfolem2  47953  paireqne  47971  prprelb  47976  prprelprb  47977  reupr  47982  reuopreuprim  47986  fmtnoprmfac1lem  48027  fmtnofac2  48032  m1expevenALTV  48123  odd2np1ALTV  48150  opoeALTV  48159  opeoALTV  48160  perfectALTVlem2  48198  isgbe  48227  isgbow  48228  isgbo  48229  sbgoldbalt  48257  sgoldbeven3prm  48259  mogoldbb  48261  nnsum3primesgbe  48268  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  isuspgrim0  48370  isuspgrimlem  48371  clnbgrgrim  48410  usgrgrtrirex  48426  stgredgel  48433  stgrusgra  48435  stgr1  48437  grlimgrtri  48479  gpgiedgdmel  48525  gpgedgel  48526  gpgprismgr4cycllem10  48580  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem4  48595  pgnbgreunbgr  48601  uspgrsprf1  48623  uspgrsprfo  48624  0nodd  48646  1odd  48647  2nodd  48648  0even  48713  1neven  48714  2even  48715  2zlidl  48716  2zrngamgm  48721  2zrngagrp  48725  2zrngmmgm  48728  2zrngnmrid  48732  suppmptcfin  48852  lcoval  48888  linc0scn0  48899  linc1  48901  el0ldep  48942  snlindsntor  48947  blenval  49047  nn0sumshdiglemB  49096  itcoval1  49139  mo0  49289  eloprab1st2nd  49343  oppcmndclem  49492  sectpropdlem  49511  invpropdlem  49513  isopropdlem  49515  upciclem1  49641  oppcup3lem  49681  isthincd2lem1  49900  termcbasmo  49958  isinito2lem  49973  arweuthinc  50004  arweutermc  50005  discsntermlem  50045  basrestermcfolem  50046