Theorem eqeq1 2743

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeq1i  2744  eqtr  2759  eqtr2  2760  iseqsetvlem  2802  eqsb1  2865  cbvexeqsetf  3446  rexraleqim  3585  eqvincf  3588  pm13.183  3604  moeq  3648  mob  3658  euind  3665  reu2eqd  3677  reuind  3694  eqsbc1  3769  sbceqal  3784  csbhypf  3859  uniiunlem  4018  snjust  4554  elsng  4569  elprg  4578  reusngf  4606  rexreusng  4611  reuprg0  4634  rabrsn  4656  preq12bg  4784  intab  4908  uniintsn  4915  dfiun2g  4959  dfiin2g  4960  disji2  5056  disjprg  5068  unopab  5152  eusv1  5320  reusv2lem2  5328  reusv3  5334  axprg  5366  opthg  5417  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  propeqop  5448  euotd  5454  otiunsndisj  5461  elopabw  5468  solin  5553  elxpi  5640  opbrop  5716  relop  5792  ideqg  5793  dmopab2rex  5859  elrnmpt  5900  elrnmpt1  5902  elrnmptg  5903  restidsing  6005  somin1  6083  cnveqb  6147  reu3op  6243  reuop  6244  ordequn  6415  iotaval2  6456  funopg  6519  f0rn0  6712  fvelrnb  6887  fvmptg  6933  fndmin  6986  eldmrexrn  7032  foelrn  7048  foelrnf  7049  foco2  7050  fmptco  7071  funopsn  7090  funopsnOLD  7091  funsndifnop  7094  fmptsng  7112  fmptsnd  7113  tpres  7145  eufnfv  7173  elabrex  7186  elabrexg  7187  abrexco  7188  f1veqaeq  7200  fpropnf1  7211  nf1const  7248  isosolem  7291  f1oiso  7295  eusvobj2  7348  oprabidw  7387  oprabid  7388  f1opr  7412  oprabv  7416  0mpo0  7439  elrnmpog  7491  elrnmpo  7492  elrnmpores  7494  ralrnmpo  7495  ov3  7519  ov6g  7520  ovelrn  7532  caovcang  7557  caovcan  7560  caofidlcan  7658  uniuni  7705  orduninsuc  7783  funcnvuni  7872  fiunlem  7884  fiun  7885  f1iun  7886  f1oweALT  7914  opiota  8001  eloprabi  8005  mpof1o2d  8065  frxp  8066  funsssuppss  8130  dftpos4  8185  tz7.44-2  8336  tz7.44-3  8337  oev  8439  oalimcl  8485  omlimcl  8503  odi  8504  omeu  8510  oeeui  8528  nneob  8582  omopth  8588  eldifsucnn  8590  elqsg  8700  qsdisj  8731  qsel  8733  brecop  8747  eroveu  8749  erovlem  8750  elixpsn  8875  ixpsnf1o  8876  boxcutc  8879  2dom  8967  fundmen  8968  xpf1o  9067  nneneq  9130  fofinf1o  9232  elfi  9316  elfiun  9333  dffi3  9334  brwdom  9472  brwdom3  9487  unwdomg  9489  xpwdomg  9490  noinfep  9572  cantnfp1lem1  9590  cantnfp1lem3  9592  cantnflem1  9601  ssttrcl  9627  ttrclselem2  9638  scott0  9801  updjudhcoinrg  9848  updjud  9849  carden2a  9881  cardiun  9897  pm54.43lem  9915  alephval3  10023  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2b  10044  kmlem9  10072  kmlem12  10075  cardcf  10165  cfeq0  10169  cfsuc  10170  cff1  10171  cflim2  10176  cfss  10178  isfin5  10212  fin1a2lem11  10323  fin1a2lem13  10325  brdom7disj  10444  brdom6disj  10445  canthp1lem2  10567  canthp1  10568  tskuni  10697  gruina  10732  genpv  10913  genpelv  10914  addsrmo  10987  mulsrmo  10988  ltsosr  11008  ltresr  11054  axcnre  11078  axpre-lttri  11079  ltordlem  11666  ltord1  11667  fimaxre3  12093  supaddc  12114  supadd  12115  supmul1  12116  supmullem1  12117  supmullem2  12118  supmul  12119  creur  12144  creui  12145  nn1m1nn  12186  elz  12517  nn0ind-raph  12620  xnegeq  13150  xmullem2  13208  xmulasslem  13228  fleqceilz  13804  fseqsupubi  13931  sqeqor  14169  nn0opth2  14225  hash1snb  14372  hash2prde  14423  prprrab  14426  hash2pwpr  14429  tpf1ofv1  14450  tpf1ofv2  14451  tpfo  14453  fi1uzind  14460  wrd2ind  14676  cshfn  14743  cshf1  14763  2cshwcshw  14778  scshwfzeqfzo  14779  pfx2  14900  s3iunsndisj  14921  relexpsucnnr  14978  relexprelg  14991  rtrclreclem3  15013  shftfval  15023  sgnval  15041  01sqrexlem6  15200  reusq0  15418  summo  15670  fsum  15673  telfsumo  15756  infcvgaux1i  15813  infcvgaux2i  15814  mertenslem1  15840  mertenslem2  15841  mertens  15842  prodmo  15892  fprod  15897  ruclem12  16199  mod2eq1n2dvds  16307  divalg  16363  ndvdssub  16369  sadcp1  16415  smupp1  16440  gcdval  16456  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  bezout  16503  lcmval  16552  coprmgcdb  16609  coprmdvds1  16612  divgcdcoprmex  16626  dvdsprime  16647  nprm  16648  dvdsprm  16664  coprm  16672  qnumval  16698  qdenval  16699  m1dvdsndvds  16760  reumodprminv  16766  pcval  16806  pceu  16808  pczpre  16809  pcdiv  16814  4sqlem2  16911  4sqlem4  16914  4sqlem12  16918  4sq  16926  vdwapval  16935  vdwapun  16936  vdwlem6  16948  cshwrepswhash1  17064  acsfn  17616  initoid  17959  termoid  17960  cat1lem  18054  posi  18274  gsumval2a  18644  smndex2dnrinv  18877  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  sgrp2nmndlem5  18891  mgmnsgrpex  18893  sgrpnmndex  18894  cyccom  19169  ghmf1  19212  conjnmzb  19219  orbsta  19279  symgextfv  19384  symgextfo  19388  symgfixfo  19405  pmtrprfval  19453  pmtrprfvalrn  19454  psgneu  19472  psgnval  19473  psgnvali  19474  psgnvalii  19475  odfval  19498  odval  19500  dfod2  19530  submod  19535  isslw  19574  sylow2alem1  19583  sylow3lem2  19594  lsmelvalm  19617  lsmdisj2  19648  efgrelexlemb  19716  frgpup3lem  19743  cyggeninv  19849  gsumval3eu  19870  gsumval3lem2  19872  gsummpt1n0  19931  nn0gsumfz  19950  dprddisj2  20007  dpjrid  20030  pgpfac1lem3  20045  rrgeq0i  20671  domneq0  20680  domnlcanb  20692  domnrcanb  20694  abveq0  20790  abvtrivd  20804  lss1d  20953  lspsn  20992  ellspsn  20993  lspprel  21084  prmirredlem  21447  znf1o  21526  znfld  21535  znunit  21538  cygznlem3  21544  psgndif  21577  ipeq0  21613  obsip  21696  frlmphl  21756  uvcvval  21761  ellspd  21777  psrlidm  21936  psrridm  21937  psrascl  21953  mvrval2  21957  mvrf1  21960  mplmonmul  22012  evlslem3  22056  selvvvval  22118  mhpsclcl  22135  psdmplcl  22150  psdmul  22154  psdmvr  22157  coe1tm  22259  coe1tmfv2  22261  cply1coe0  22287  cply1coe0bi  22288  gsummoncoe1  22294  mamufacex  22379  mat1comp  22423  mat1dimelbas  22454  mat1dimid  22457  scmatel  22488  scmateALT  22495  mavmulsolcl  22534  marrepeval  22546  marepveval  22551  mdetunilem8  22602  maducoeval2  22623  madugsum  22626  minmar1eval  22632  symgmatr01lem  22636  symgmatr01  22637  gsummatr01lem3  22640  gsummatr01lem4  22641  gsummatr01  22642  m2cpm  22724  m2cpminvid2lem  22737  decpmatid  22753  monmatcollpw  22762  pmatcollpw3fi1lem1  22769  mp2pm2mplem4  22792  fvmptnn04ifc  22835  chfacffsupp  22839  chfacfscmul0  22841  chfacfscmulgsum  22843  chfacfpmmul0  22845  chfacfpmmulgsum  22847  cpmadumatpoly  22866  cayleyhamilton  22873  cayleyhamiltonALT  22874  istopon  22895  toponsspwpw  22905  fctop  22987  cctop  22989  ppttop  22990  pptbas  22991  epttop  22992  t0sep  23307  t1sep2  23352  cmpsublem  23382  cmpsub  23383  unisngl  23510  txuni2  23548  elpt  23555  ptbasfi  23564  xkoopn  23572  ptpjopn  23595  ptclsg  23598  dfac14lem  23600  ptcnp  23605  ptrescn  23622  tx1stc  23633  qtopeu  23699  kqt0lem  23719  isr0  23720  hauspwpwf1  23970  xmeteq0  24321  imasf1oxmet  24358  comet  24496  stdbdxmet  24498  met2ndci  24505  prdsxmslem2  24512  nrmmetd  24557  tngngp  24637  tngngp3  24639  xrsxmet  24793  iccpnfcnv  24929  iccpnfhmeo  24930  cnheibor  24940  elovolm  25460  ovolgelb  25465  ovolicc1  25501  ovolicc  25508  ioorval  25559  uniioombllem6  25573  dyadmax  25583  dyadmbl  25585  i1fadd  25680  i1fmul  25681  itg1addlem3  25683  i1fmulc  25688  itg2l  25714  itg2leub  25719  limcmpt  25868  limcco  25878  dvcobr  25931  deg1ldg  26075  ig1pval  26159  elply  26178  elply2  26179  coeval  26206  coe1termlem  26241  coe1term  26242  quotval  26276  plydivlem4  26280  plydivex  26281  vieta1  26296  aannenlem2  26313  aalioulem2  26317  abelthlem9  26423  logtayllem  26641  logtayl  26642  isosctrlem2  26801  leibpilem2  26923  rlimcnp2  26948  efrlim  26951  mpodvdsmulf1o  27175  dvdsmulf1o  27177  perfectlem2  27211  lgsfval  27283  lgsval2lem  27288  lgsqrmodndvds  27334  lgsdchrval  27335  gausslemma2dlem0i  27345  2lgslem1b  27373  2lgslem3  27385  2sqlem2  27399  2sqlem8  27407  2sqlem9  27408  2sqlem11  27410  addsq2reu  27421  dchrisum0flblem1  27489  padicval  27598  padicabv  27611  ostth1  27614  ltsval2  27638  ltsintdifex  27643  ltsres  27644  nolt02o  27677  madef  27846  addsval2  27973  addsproplem2  27980  addsproplem4  27982  addsproplem5  27983  addsproplem6  27984  addsprop  27986  addcuts  27988  leadds1  27999  addsuniflem  28011  addsunif  28012  addsasslem1  28013  addsasslem2  28014  addbdaylem  28027  negsprop  28045  negsid  28051  mulsval2lem  28120  mulsproplem9  28134  mulsproplem12  28137  mulsprop  28140  sltmuls1  28157  sltmuls2  28158  mulsuniflem  28159  addsdilem1  28161  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  mulsunif2  28180  precsexlemcbv  28216  precsexlem9  28225  precsexlem11  28227  n0s0suc  28352  onsfi  28366  n0s0m1  28372  nn1m1nns  28384  eucliddivs  28386  n0seo  28431  zseo  28432  expsval  28435  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  bdayfinbnd  28479  elz12s  28482  z12zsodd  28492  z12sge0  28493  recut  28504  elreno2  28505  renegscl  28508  readdscl  28509  remulscllem1  28510  remulscl  28512  axtgcgrid  28549  axtgbtwnid  28552  islmib  28873  inaghl  28931  axpaschlem  29027  axlowdimlem15  29043  axlowdim  29048  upgredg2vtx  29228  edglnl  29230  umgredgnlp  29234  usgredg2vtxeuALT  29309  uspgredg2v  29311  ushgredgedgloop  29318  nbusgredgeu  29453  cusgrfilem2  29543  cusgrfi  29545  vtxdushgrfvedg  29577  1loopgrvd2  29590  rusgr1vtxlem  29674  wlkeq  29720  wlkp1lem8  29765  upgrwlkdvdelem  29822  crctcshwlkn0lem6  29901  wlknwwlksnbij  29974  rusgrnumwwlkl1  30057  clwlkclwwlklem2a1  30080  clwwlknscsh  30150  eleclclwwlkn  30164  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon1sn  30188  frgr3vlem1  30361  3vfriswmgrlem  30365  frgrncvvdeqlem3  30389  wlkl0  30455  frgrreggt1  30481  nvz  30758  nmosetn0  30854  nmoolb  30860  nmoubi  30861  nmlno0lem  30882  nmlno0i  30883  hvsubeq0  31157  hvaddcan  31159  normsub0  31225  norm1exi  31339  pjhval  31486  omlsii  31492  omlsi  31493  pjoml  31525  h1de2ci  31645  spansneleq  31659  h1datomi  31670  h1datom  31671  spansncv  31742  5oalem6  31748  pj11  31803  nmopsetn0  31954  nmfnsetn0  31967  nmoplb  31996  nmopub  31997  nmfnlb  32013  nmfnleub  32014  nmlnop0iALT  32084  nmlnop0  32087  lnopeq  32098  nmopun  32103  nmcexi  32115  branmfn  32194  pjnmopi  32237  pj3i  32297  atss  32435  atom1d  32442  chirred  32484  cdj3lem2  32524  eqelbid  32562  elabreximd  32598  disjxpin  32677  disjunsn  32683  br8d  32700  fmptcof2  32749  sgn3da  32926  sgnmul  32927  sgnnbi  32930  sgnpbi  32931  sgn0bi  32932  psgnfzto1stlem  33181  sgnsval  33242  elrgspnlem2  33324  elrgspnlem3  33325  domnlcanOLD  33361  linds2eq  33464  elrspunsn  33512  mxidlmax  33548  1arithidomlem1  33618  1arithidom  33620  1arithufdlem1  33627  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  1arithufd  33631  dfufd2  33633  ply1dg1rt  33663  selvply1rhmlem2  33705  mplvrpmrhm  33731  psrmonmul  33734  esplyfvaln  33758  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  rtelextdg2lem  33910  constrsuc  33922  constrcbvlem  33939  2sqr3minply  33964  madjusmdetlem2  34012  madjusmdet  34015  zarclssn  34057  xrge0iifcnv  34117  xrge0iifcv  34118  xrge0iifhom  34121  xrge0tmd  34129  xrge0tmdALT  34130  esumc  34235  plymulx0  34731  signspval  34736  tgoldbachgt  34847  bnj1468  35028  fineqvnttrclselem3  35304  fineqvnttrclse  35305  f1resfz0f1d  35342  acycgrcycl  35375  sconnpi1  35467  cvmlift3lem2  35548  satfv0  35586  satfv1  35591  satfbrsuc  35594  satfrnmapom  35598  satfv0fun  35599  satf0op  35605  sat1el2xp  35607  fmlafvel  35613  fmla1  35615  isfmlasuc  35616  fmlaomn0  35618  gonan0  35620  goaln0  35621  gonar  35623  goalr  35625  fmla0disjsuc  35626  fmlasucdisj  35627  satffunlem1lem1  35630  satffunlem2lem1  35632  dmopab3rexdif  35633  satfv0fvfmla0  35641  sategoelfvb  35647  ex-sategoelel  35649  satfv1fvfmla1  35651  2goelgoanfmla1  35652  ex-sategoelelomsuc  35654  ex-sategoelel12  35655  prv1n  35659  ellcsrspsn  35869  r1peuqusdeg1  35871  br8  35984  br6  35985  br4  35986  rdgprc0  36019  dfrdg2  36021  dfbigcup2  36125  elsingles  36144  dfiota3  36149  brimageg  36153  brdomaing  36161  brrangeg  36162  dfrdg4  36179  elaltxp  36203  funtransport  36259  fvtransport  36260  brsegle  36336  funray  36368  fvray  36369  funline  36370  fvline  36372  ellines  36380  linethru  36381  rankeq1o  36399  subtr  36542  subtr2  36543  nn0prpw  36551  bj-elabd2ALT  37278  bj-gabss  37288  bj-imafv  37611  topdifinffinlem  37709  topdifinffin  37710  topdifinfeq  37712  finxpreclem2  37752  finxpreclem3  37755  fvineqsnf1  37772  fvineqsneu  37773  wl-ax12v2cl  37868  wl-dfclel  37877  wl-issetft  37953  fin2so  37974  ptrest  37986  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem31  38018  poimirlem32  38019  heicant  38022  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  ftc1anc  38068  unirep  38081  sdclem2  38109  sdclem1  38110  sdc  38111  fdc  38112  isbnd  38147  heibor1lem  38176  heiborlem4  38181  heiborlem6  38183  heiborlem10  38187  ismgmOLD  38217  maxidlmax  38410  prnc  38434  isfldidl  38435  dmnnzd  38442  disjressuc2  38778  qsdisjALTV  39066  eqvrelqsel  39067  riotasvd  39448  lshpdisj  39479  lsat0cv  39525  lcvexchlem4  39529  lcvexchlem5  39530  lshpkrlem1  39602  lshpkrlem2  39603  lshpkrlem3  39604  lshpkrcl  39608  islshpkrN  39612  atnle  39809  glbconxN  39870  isline  40231  ispointN  40234  pmapglbx  40261  ispsubcl2N  40439  lhp2atnle  40525  cdleme43fsv1snlem  40912  cdleme40v  40961  cdlemkid5  41427  cdlemkid  41428  dvhb1dimN  41478  dib1dim  41657  dicopelval  41669  dicelval1sta  41679  diclspsn  41686  dihvalcqpre  41727  dihglblem2aN  41785  dihglblem2N  41786  dih1dimatlem  41821  dihpN  41828  dochfl1  41968  lcfl7N  41993  lcf1o  42043  hvmapvalvalN  42253  hdmapval2lem  42323  aks6d1c1  42601  aks6d1c4  42609  sticksstones10  42640  sticksstones12a  42642  aks6d1c7  42669  sn-iotalem  42708  fiabv  43022  evlsbagval  43036  fsuppind  43040  absnw  43128  elrfi  43143  nacsfg  43154  mzpcompact2lem  43200  eldioph2b  43212  eldioph3  43215  eldiophss  43223  diophrex  43224  elnn0rabdioph  43248  rencldnfilem  43265  elpell1qr  43292  elpell14qr  43294  elpell1234qr  43296  jm2.27  43453  rmydioph  43459  expdiophlem2  43467  wepwsolem  43487  aomclem6  43504  lnr2i  43561  lpirlnr  43562  hbtlem2  43569  hbtlem4  43571  hbtlem5  43573  rngunsnply  43614  flcidc  43615  onsucelab  43708  limnsuc  43710  nnoeomeqom  43757  cantnfresb  43769  tfsconcatfv2  43785  tfsconcatb0  43789  oaun3lem1  43819  oadif1lem  43824  oadif1  43825  clcnvlem  44067  brtrclfv2  44171  frege55lem1c  44360  frege104  44411  clsk1indlem0  44485  clsk1indlem2  44486  clsk1indlem3  44487  clsk1indlem4  44488  clsk1indlem1  44489  pm13.192  44854  equncomVD  45311  csbingVD  45327  csbsngVD  45336  csbfv12gALTVD  45342  relopabVD  45344  refsum2cnlem1  45485  elrnmptf  45628  upbdrech  45753  ssfiunibd  45757  iccshift  45963  iooshift  45967  fsumf1of  46019  limcperiod  46073  climinf2mpt  46157  climinfmpt  46158  cncfshiftioo  46335  itgiccshift  46423  itgperiod  46424  stoweidlem46  46489  fourierdlem29  46579  fourierdlem37  46587  fourierdlem48  46597  fourierdlem51  46600  fourierdlem54  46603  fourierdlem62  46611  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem92  46641  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem103  46652  fourierdlem104  46653  fourierdlem105  46654  fourierdlem108  46657  fourierdlem110  46659  fourierdlem112  46661  etransclem1  46678  etransclem5  46682  etransclem17  46694  etransclem32  46709  etransclem41  46718  sge0f1o  46825  sge0resplit  46849  sge0fodjrnlem  46859  nnfoctbdjlem  46898  nnfoctbdj  46899  ovnval  46984  ovnlecvr  47001  ovnpnfelsup  47002  ovn0lem  47008  hoidmvval  47020  hoidmvlelem1  47038  ovnhoilem1  47044  ovnhoi  47046  ovnlecvr2  47053  hoidifhspval3  47062  hspmbllem2  47070  hoimbl  47074  ovnsubadd2  47089  ovolval5lem2  47096  ovolval5lem3  47097  ovolval5  47098  ovnovol  47102  sinnpoly  47354  fsetsnf  47514  fsetsnfo  47516  fcoresf1  47532  aiotaval  47558  euoreqb  47572  afv0fv0  47612  afvfv0bi  47615  afvelrnb  47626  afvelrnb0  47627  afv20defat  47695  otiunsndisjX  47742  fun2dmnopgexmpl  47747  2ffzoeq  47791  modmkpkne  47830  elsetpreimafvb  47859  imasetpreimafvbijlemfo  47880  fargshiftf1  47916  fargshiftfo  47917  ichnreuop  47947  ichreuopeq  47948  elsprel  47950  spr0nelg  47951  sprel  47959  prelspr  47961  sprsymrelf1lem  47966  sprsymrelfolem2  47968  paireqne  47986  prprelb  47991  prprelprb  47992  reupr  47997  reuopreuprim  48001  fmtnoprmfac1lem  48042  fmtnofac2  48047  m1expevenALTV  48138  odd2np1ALTV  48165  opoeALTV  48174  opeoALTV  48175  perfectALTVlem2  48213  isgbe  48242  isgbow  48243  isgbo  48244  sbgoldbalt  48272  sgoldbeven3prm  48274  mogoldbb  48276  nnsum3primesgbe  48283  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  vopnbgrel  48345  dfclnbgr6  48347  dfnbgr6  48348  isuspgrim0  48385  isuspgrimlem  48386  clnbgrgrim  48425  usgrgrtrirex  48441  stgredgel  48448  stgrusgra  48450  stgr1  48452  grlimgrtri  48494  gpgiedgdmel  48540  gpgedgel  48541  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem4  48610  pgnbgreunbgr  48616  uspgrsprf1  48638  uspgrsprfo  48639  0nodd  48661  1odd  48662  2nodd  48663  0even  48728  1neven  48729  2even  48730  2zlidl  48731  2zrngamgm  48736  2zrngagrp  48740  2zrngmmgm  48743  2zrngnmrid  48747  suppmptcfin  48867  lcoval  48903  linc0scn0  48914  linc1  48916  el0ldep  48957  snlindsntor  48962  blenval  49062  nn0sumshdiglemB  49111  itcoval1  49154  mo0  49304  eloprab1st2nd  49358  oppcmndclem  49507  sectpropdlem  49526  invpropdlem  49528  isopropdlem  49530  upciclem1  49656  oppcup3lem  49696  isthincd2lem1  49915  termcbasmo  49973  isinito2lem  49988  arweuthinc  50019  arweutermc  50020  discsntermlem  50060  basrestermcfolem  50061