Theorem eqeq1 2741

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 2739	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 2709

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

This theorem is referenced by:  eqeq1i  2742  eqtr  2757  eqtr2  2758  iseqsetvlem  2800  eqsb1  2863  cbvexeqsetf  3457  cgsex4gOLD  3490  rexraleqim  3603  eqvincf  3606  pm13.183  3622  moeq  3667  mob  3677  euind  3684  reu2eqd  3696  reuind  3713  eqsbc1  3789  sbceqal  3804  csbhypf  3879  uniiunlem  4041  snjust  4581  elsng  4596  elprg  4605  reusngf  4633  rexreusng  4638  reuprg0  4661  rabrsn  4683  preq12bg  4811  intab  4935  uniintsn  4942  dfiun2g  4987  dfiin2g  4988  disji2  5084  disjprg  5096  unopab  5180  eusv1  5338  reusv2lem2  5346  reusv3  5352  axprg  5383  opthg  5433  copsexgw  5446  copsexg  5447  propeqop  5463  euotd  5469  otiunsndisj  5476  elopabw  5482  solin  5567  elxpi  5654  opbrop  5730  relop  5807  ideqg  5808  dmopab2rex  5874  elrnmpt  5915  elrnmpt1  5917  elrnmptg  5918  restidsing  6020  somin1  6098  cnveqb  6162  reu3op  6258  reuop  6259  ordequn  6430  iotaval2  6471  funopg  6534  f0rn0  6727  fvelrnb  6902  fvmptg  6947  fndmin  6999  eldmrexrn  7045  foelrn  7061  foelrnf  7062  foco2  7063  fmptco  7084  funopsn  7103  funsndifnop  7106  fmptsng  7124  fmptsnd  7125  tpres  7157  eufnfv  7185  elabrex  7198  elabrexg  7199  abrexco  7200  f1veqaeq  7212  fpropnf1  7223  nf1const  7260  isosolem  7303  f1oiso  7307  eusvobj2  7360  oprabidw  7399  oprabid  7400  f1opr  7424  oprabv  7428  0mpo0  7451  elrnmpog  7503  elrnmpo  7504  elrnmpores  7506  ralrnmpo  7507  ov3  7531  ov6g  7532  ovelrn  7544  caovcang  7569  caovcan  7572  caofidlcan  7670  uniuni  7717  orduninsuc  7795  funcnvuni  7884  fiunlem  7896  fiun  7897  f1iun  7898  f1oweALT  7926  opiota  8013  eloprabi  8017  frxp  8078  funsssuppss  8142  dftpos4  8197  tz7.44-2  8348  tz7.44-3  8349  oev  8451  oalimcl  8497  omlimcl  8515  odi  8516  omeu  8522  oeeui  8540  nneob  8594  omopth  8600  eldifsucnn  8602  elqsg  8712  qsdisj  8743  qsel  8745  brecop  8759  eroveu  8761  erovlem  8762  elixpsn  8887  ixpsnf1o  8888  boxcutc  8891  2dom  8979  fundmen  8980  xpf1o  9079  nneneq  9142  fofinf1o  9244  elfi  9328  elfiun  9345  dffi3  9346  brwdom  9484  brwdom3  9499  unwdomg  9501  xpwdomg  9502  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  11674  ltord1  11675  fimaxre3  12100  supaddc  12121  supadd  12122  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  creur  12151  creui  12152  nn1m1nn  12178  elz  12502  nn0ind-raph  12604  xnegeq  13134  xmullem2  13192  xmulasslem  13212  fleqceilz  13786  fseqsupubi  13913  sqeqor  14151  nn0opth2  14207  hash1snb  14354  hash2prde  14405  prprrab  14408  hash2pwpr  14411  tpf1ofv1  14432  tpf1ofv2  14433  tpfo  14435  fi1uzind  14442  wrd2ind  14658  cshfn  14725  cshf1  14745  2cshwcshw  14760  scshwfzeqfzo  14761  pfx2  14882  s3iunsndisj  14903  relexpsucnnr  14960  relexprelg  14973  rtrclreclem3  14995  shftfval  15005  sgnval  15023  01sqrexlem6  15182  reusq0  15400  summo  15652  fsum  15655  telfsumo  15737  infcvgaux1i  15792  infcvgaux2i  15793  mertenslem1  15819  mertenslem2  15820  mertens  15821  prodmo  15871  fprod  15876  ruclem12  16178  mod2eq1n2dvds  16286  divalg  16342  ndvdssub  16348  sadcp1  16394  smupp1  16419  gcdval  16435  bezoutlem1  16478  bezoutlem3  16480  bezoutlem4  16481  bezout  16482  lcmval  16531  coprmgcdb  16588  coprmdvds1  16591  divgcdcoprmex  16605  dvdsprime  16626  nprm  16627  dvdsprm  16642  coprm  16650  qnumval  16676  qdenval  16677  m1dvdsndvds  16738  reumodprminv  16744  pcval  16784  pceu  16786  pczpre  16787  pcdiv  16792  4sqlem2  16889  4sqlem4  16892  4sqlem12  16896  4sq  16904  vdwapval  16913  vdwapun  16914  vdwlem6  16926  cshwrepswhash1  17042  acsfn  17594  initoid  17937  termoid  17938  cat1lem  18032  posi  18252  gsumval2a  18622  smndex2dnrinv  18852  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  sgrp2nmndlem5  18866  mgmnsgrpex  18868  sgrpnmndex  18869  cyccom  19144  ghmf1  19187  conjnmzb  19194  orbsta  19254  symgextfv  19359  symgextfo  19363  symgfixfo  19380  pmtrprfval  19428  pmtrprfvalrn  19429  psgneu  19447  psgnval  19448  psgnvali  19449  psgnvalii  19450  odfval  19473  odval  19475  dfod2  19505  submod  19510  isslw  19549  sylow2alem1  19558  sylow3lem2  19569  lsmelvalm  19592  lsmdisj2  19623  efgrelexlemb  19691  frgpup3lem  19718  cyggeninv  19824  gsumval3eu  19845  gsumval3lem2  19847  gsummpt1n0  19906  nn0gsumfz  19925  dprddisj2  19982  dpjrid  20005  pgpfac1lem3  20020  rrgeq0i  20644  domneq0  20653  domnlcanb  20665  domnrcanb  20667  abveq0  20763  abvtrivd  20777  lss1d  20926  lspsn  20965  ellspsn  20966  lspprel  21058  prmirredlem  21439  znf1o  21518  znfld  21527  znunit  21530  cygznlem3  21536  psgndif  21569  ipeq0  21605  obsip  21688  frlmphl  21748  uvcvval  21753  ellspd  21769  psrlidm  21929  psrridm  21930  psrascl  21946  mvrval2  21950  mvrf1  21953  mplmonmul  22003  evlslem3  22047  mhpsclcl  22102  psdmplcl  22117  psdmul  22121  psdmvr  22124  coe1tm  22227  coe1tmfv2  22229  cply1coe0  22257  cply1coe0bi  22258  gsummoncoe1  22264  mamufacex  22352  mat1comp  22396  mat1dimelbas  22427  mat1dimid  22430  scmatel  22461  scmateALT  22468  mavmulsolcl  22507  marrepeval  22519  marepveval  22524  mdetunilem8  22575  maducoeval2  22596  madugsum  22599  minmar1eval  22605  symgmatr01lem  22609  symgmatr01  22610  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  m2cpm  22697  m2cpminvid2lem  22710  decpmatid  22726  monmatcollpw  22735  pmatcollpw3fi1lem1  22742  mp2pm2mplem4  22765  fvmptnn04ifc  22808  chfacffsupp  22812  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  cpmadumatpoly  22839  cayleyhamilton  22846  cayleyhamiltonALT  22847  istopon  22868  toponsspwpw  22878  fctop  22960  cctop  22962  ppttop  22963  pptbas  22964  epttop  22965  t0sep  23280  t1sep2  23325  cmpsublem  23355  cmpsub  23356  unisngl  23483  txuni2  23521  elpt  23528  ptbasfi  23537  xkoopn  23545  ptpjopn  23568  ptclsg  23571  dfac14lem  23573  ptcnp  23578  ptrescn  23595  tx1stc  23606  qtopeu  23672  kqt0lem  23692  isr0  23693  hauspwpwf1  23943  xmeteq0  24294  imasf1oxmet  24331  comet  24469  stdbdxmet  24471  met2ndci  24478  prdsxmslem2  24485  nrmmetd  24530  tngngp  24610  tngngp3  24612  xrsxmet  24766  iccpnfcnv  24910  iccpnfhmeo  24911  cnheibor  24922  elovolm  25444  ovolgelb  25449  ovolicc1  25485  ovolicc  25492  ioorval  25543  uniioombllem6  25557  dyadmax  25567  dyadmbl  25569  i1fadd  25664  i1fmul  25665  itg1addlem3  25667  i1fmulc  25672  itg2l  25698  itg2leub  25703  limcmpt  25852  limcco  25862  dvcobr  25917  dvcobrOLD  25918  deg1ldg  26065  ig1pval  26149  elply  26168  elply2  26169  coeval  26196  coe1termlem  26231  coe1term  26232  quotval  26268  plydivlem4  26272  plydivex  26273  vieta1  26288  aannenlem2  26305  aalioulem2  26309  abelthlem9  26418  logtayllem  26636  logtayl  26637  isosctrlem2  26797  leibpilem2  26919  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  mpodvdsmulf1o  27172  dvdsmulf1o  27174  perfectlem2  27209  lgsfval  27281  lgsval2lem  27286  lgsqrmodndvds  27332  lgsdchrval  27333  gausslemma2dlem0i  27343  2lgslem1b  27371  2lgslem3  27383  2sqlem2  27397  2sqlem8  27405  2sqlem9  27406  2sqlem11  27408  addsq2reu  27419  dchrisum0flblem1  27487  padicval  27596  padicabv  27609  ostth1  27612  ltsval2  27636  ltsintdifex  27641  ltsres  27642  nolt02o  27675  madef  27844  addsval2  27971  addsproplem2  27978  addsproplem4  27980  addsproplem5  27981  addsproplem6  27982  addsprop  27984  addcuts  27986  leadds1  27997  addsuniflem  28009  addsunif  28010  addsasslem1  28011  addsasslem2  28012  addbdaylem  28025  negsprop  28043  negsid  28049  mulsval2lem  28118  mulsproplem9  28132  mulsproplem12  28135  mulsprop  28138  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  mulsunif2  28178  precsexlemcbv  28214  precsexlem9  28223  precsexlem11  28225  n0s0suc  28350  onsfi  28364  n0s0m1  28370  nn1m1nns  28382  eucliddivs  28384  n0seo  28429  zseo  28430  expsval  28433  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  bdayfinbnd  28477  elz12s  28480  z12zsodd  28490  z12sge0  28491  recut  28502  elreno2  28503  renegscl  28506  readdscl  28507  remulscllem1  28508  remulscl  28510  axtgcgrid  28547  axtgbtwnid  28550  islmib  28871  inaghl  28929  axpaschlem  29025  axlowdimlem15  29041  axlowdim  29046  upgredg2vtx  29226  edglnl  29228  umgredgnlp  29232  usgredg2vtxeuALT  29307  uspgredg2v  29309  ushgredgedgloop  29316  nbusgredgeu  29451  cusgrfilem2  29542  cusgrfi  29544  vtxdushgrfvedg  29576  1loopgrvd2  29589  rusgr1vtxlem  29673  wlkeq  29719  wlkp1lem8  29764  upgrwlkdvdelem  29821  crctcshwlkn0lem6  29900  wlknwwlksnbij  29973  rusgrnumwwlkl1  30056  clwlkclwwlklem2a1  30079  clwwlknscsh  30149  eleclclwwlkn  30163  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon1sn  30187  frgr3vlem1  30360  3vfriswmgrlem  30364  frgrncvvdeqlem3  30388  wlkl0  30454  frgrreggt1  30480  nvz  30757  nmosetn0  30853  nmoolb  30859  nmoubi  30860  nmlno0lem  30881  nmlno0i  30882  hvsubeq0  31156  hvaddcan  31158  normsub0  31224  norm1exi  31338  pjhval  31485  omlsii  31491  omlsi  31492  pjoml  31524  h1de2ci  31644  spansneleq  31658  h1datomi  31669  h1datom  31670  spansncv  31741  5oalem6  31747  pj11  31802  nmopsetn0  31953  nmfnsetn0  31966  nmoplb  31995  nmopub  31996  nmfnlb  32012  nmfnleub  32013  nmlnop0iALT  32083  nmlnop0  32086  lnopeq  32097  nmopun  32102  nmcexi  32114  branmfn  32193  pjnmopi  32236  pj3i  32296  atss  32434  atom1d  32441  chirred  32483  cdj3lem2  32523  eqelbid  32561  elabreximd  32597  disjxpin  32675  disjunsn  32681  br8d  32698  fmptcof2  32747  sgn3da  32926  sgnmul  32927  sgnnbi  32930  sgnpbi  32931  sgn0bi  32932  psgnfzto1stlem  33194  sgnsval  33255  elrgspnlem2  33337  elrgspnlem3  33338  domnlcanOLD  33374  linds2eq  33474  elrspunsn  33522  mxidlmax  33558  1arithidomlem1  33628  1arithidom  33630  1arithufdlem1  33637  1arithufdlem2  33638  1arithufdlem3  33639  1arithufdlem4  33640  1arithufd  33641  dfufd2  33643  ply1dg1rt  33673  mplvrpmrhm  33724  psrmonmul  33727  esplyfvaln  33751  lbsdiflsp0  33804  fedgmullem1  33807  fedgmullem2  33808  rtelextdg2lem  33904  constrsuc  33916  constrcbvlem  33933  2sqr3minply  33958  madjusmdetlem2  34006  madjusmdet  34009  zarclssn  34051  xrge0iifcnv  34111  xrge0iifcv  34112  xrge0iifhom  34115  xrge0tmd  34123  xrge0tmdALT  34124  esumc  34229  plymulx0  34725  signspval  34730  tgoldbachgt  34841  bnj1468  35022  fineqvnttrclselem3  35301  fineqvnttrclse  35302  f1resfz0f1d  35330  acycgrcycl  35363  sconnpi1  35455  cvmlift3lem2  35536  satfv0  35574  satfv1  35579  satfbrsuc  35582  satfrnmapom  35586  satfv0fun  35587  satf0op  35593  sat1el2xp  35595  fmlafvel  35601  fmla1  35603  isfmlasuc  35604  fmlaomn0  35606  gonan0  35608  goaln0  35609  gonar  35611  goalr  35613  fmla0disjsuc  35614  fmlasucdisj  35615  satffunlem1lem1  35618  satffunlem2lem1  35620  dmopab3rexdif  35621  satfv0fvfmla0  35629  sategoelfvb  35635  ex-sategoelel  35637  satfv1fvfmla1  35639  2goelgoanfmla1  35640  ex-sategoelelomsuc  35642  ex-sategoelel12  35643  prv1n  35647  ellcsrspsn  35857  r1peuqusdeg1  35859  br8  35972  br6  35973  br4  35974  rdgprc0  36007  dfrdg2  36009  dfbigcup2  36113  elsingles  36132  dfiota3  36137  brimageg  36141  brdomaing  36149  brrangeg  36150  dfrdg4  36167  elaltxp  36191  funtransport  36247  fvtransport  36248  brsegle  36324  funray  36356  fvray  36357  funline  36358  fvline  36360  ellines  36368  linethru  36369  rankeq1o  36387  subtr  36530  subtr2  36531  nn0prpw  36539  bj-elabd2ALT  37173  bj-gabss  37183  bj-imafv  37506  topdifinffinlem  37602  topdifinffin  37603  topdifinfeq  37605  finxpreclem2  37645  finxpreclem3  37648  fvineqsnf1  37665  fvineqsneu  37666  wl-ax12v2cl  37761  wl-issetft  37837  fin2so  37858  ptrest  37870  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem28  37899  poimirlem31  37902  poimirlem32  37903  heicant  37906  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  ftc1anc  37952  unirep  37965  sdclem2  37993  sdclem1  37994  sdc  37995  fdc  37996  isbnd  38031  heibor1lem  38060  heiborlem4  38065  heiborlem6  38067  heiborlem10  38071  ismgmOLD  38101  maxidlmax  38294  prnc  38318  isfldidl  38319  dmnnzd  38326  disjressuc2  38662  qsdisjALTV  38950  eqvrelqsel  38951  riotasvd  39332  lshpdisj  39363  lsat0cv  39409  lcvexchlem4  39413  lcvexchlem5  39414  lshpkrlem1  39486  lshpkrlem2  39487  lshpkrlem3  39488  lshpkrcl  39492  islshpkrN  39496  atnle  39693  glbconxN  39754  isline  40115  ispointN  40118  pmapglbx  40145  ispsubcl2N  40323  lhp2atnle  40409  cdleme43fsv1snlem  40796  cdleme40v  40845  cdlemkid5  41311  cdlemkid  41312  dvhb1dimN  41362  dib1dim  41541  dicopelval  41553  dicelval1sta  41563  diclspsn  41570  dihvalcqpre  41611  dihglblem2aN  41669  dihglblem2N  41670  dih1dimatlem  41705  dihpN  41712  dochfl1  41852  lcfl7N  41877  lcf1o  41927  hvmapvalvalN  42137  hdmapval2lem  42207  aks6d1c1  42486  aks6d1c4  42494  sticksstones10  42525  sticksstones12a  42527  aks6d1c7  42554  sn-iotalem  42593  f1o2d2  42605  fiabv  42906  evlsbagval  42927  selvvvval  42943  fsuppind  42948  absnw  43036  elrfi  43051  nacsfg  43062  mzpcompact2lem  43108  eldioph2b  43120  eldioph3  43123  eldiophss  43131  diophrex  43132  elnn0rabdioph  43160  rencldnfilem  43177  elpell1qr  43204  elpell14qr  43206  elpell1234qr  43208  jm2.27  43365  rmydioph  43371  expdiophlem2  43379  wepwsolem  43399  aomclem6  43416  lnr2i  43473  lpirlnr  43474  hbtlem2  43481  hbtlem4  43483  hbtlem5  43485  rngunsnply  43526  flcidc  43527  onsucelab  43620  limnsuc  43622  nnoeomeqom  43669  cantnfresb  43681  tfsconcatfv2  43697  tfsconcatb0  43701  oaun3lem1  43731  oadif1lem  43736  oadif1  43737  clcnvlem  43979  brtrclfv2  44083  frege55lem1c  44272  frege104  44323  clsk1indlem0  44397  clsk1indlem2  44398  clsk1indlem3  44399  clsk1indlem4  44400  clsk1indlem1  44401  pm13.192  44766  equncomVD  45223  csbingVD  45239  csbsngVD  45248  csbfv12gALTVD  45254  relopabVD  45256  refsum2cnlem1  45397  elrnmptf  45540  upbdrech  45667  ssfiunibd  45671  iccshift  45878  iooshift  45882  fsumf1of  45934  limcperiod  45988  climinf2mpt  46072  climinfmpt  46073  cncfshiftioo  46250  itgiccshift  46338  itgperiod  46339  stoweidlem46  46404  fourierdlem29  46494  fourierdlem37  46502  fourierdlem48  46512  fourierdlem51  46515  fourierdlem54  46518  fourierdlem62  46526  fourierdlem79  46543  fourierdlem81  46545  fourierdlem82  46546  fourierdlem92  46556  fourierdlem96  46560  fourierdlem97  46561  fourierdlem98  46562  fourierdlem99  46563  fourierdlem103  46567  fourierdlem104  46568  fourierdlem105  46569  fourierdlem108  46572  fourierdlem110  46574  fourierdlem112  46576  etransclem1  46593  etransclem5  46597  etransclem17  46609  etransclem32  46624  etransclem41  46633  sge0f1o  46740  sge0resplit  46764  sge0fodjrnlem  46774  nnfoctbdjlem  46813  nnfoctbdj  46814  ovnval  46899  ovnlecvr  46916  ovnpnfelsup  46917  ovn0lem  46923  hoidmvval  46935  hoidmvlelem1  46953  ovnhoilem1  46959  ovnhoi  46961  ovnlecvr2  46968  hoidifhspval3  46977  hspmbllem2  46985  hoimbl  46989  ovnsubadd2  47004  ovolval5lem2  47011  ovolval5lem3  47012  ovolval5  47013  ovnovol  47017  sinnpoly  47251  fsetsnf  47411  fsetsnfo  47413  fcoresf1  47429  aiotaval  47455  euoreqb  47469  afv0fv0  47509  afvfv0bi  47512  afvelrnb  47523  afvelrnb0  47524  afv20defat  47592  otiunsndisjX  47639  fun2dmnopgexmpl  47644  2ffzoeq  47687  modmkpkne  47721  elsetpreimafvb  47744  imasetpreimafvbijlemfo  47765  fargshiftf1  47801  fargshiftfo  47802  ichnreuop  47832  ichreuopeq  47833  elsprel  47835  spr0nelg  47836  sprel  47844  prelspr  47846  sprsymrelf1lem  47851  sprsymrelfolem2  47853  paireqne  47871  prprelb  47876  prprelprb  47877  reupr  47882  reuopreuprim  47886  fmtnoprmfac1lem  47924  fmtnofac2  47929  m1expevenALTV  48007  odd2np1ALTV  48034  opoeALTV  48043  opeoALTV  48044  perfectALTVlem2  48082  isgbe  48111  isgbow  48112  isgbo  48113  sbgoldbalt  48141  sgoldbeven3prm  48143  mogoldbb  48145  nnsum3primesgbe  48152  nnsum3primesle9  48154  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  vopnbgrel  48214  dfclnbgr6  48216  dfnbgr6  48217  isuspgrim0  48254  isuspgrimlem  48255  clnbgrgrim  48294  usgrgrtrirex  48310  stgredgel  48317  stgrusgra  48319  stgr1  48321  grlimgrtri  48363  gpgiedgdmel  48409  gpgedgel  48410  gpgprismgr4cycllem10  48464  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem4  48479  pgnbgreunbgr  48485  uspgrsprf1  48507  uspgrsprfo  48508  0nodd  48530  1odd  48531  2nodd  48532  0even  48597  1neven  48598  2even  48599  2zlidl  48600  2zrngamgm  48605  2zrngagrp  48609  2zrngmmgm  48612  2zrngnmrid  48616  suppmptcfin  48736  lcoval  48772  linc0scn0  48783  linc1  48785  el0ldep  48826  snlindsntor  48831  blenval  48931  nn0sumshdiglemB  48980  itcoval1  49023  mo0  49173  eloprab1st2nd  49227  oppcmndclem  49376  sectpropdlem  49395  invpropdlem  49397  isopropdlem  49399  upciclem1  49525  oppcup3lem  49565  isthincd2lem1  49784  termcbasmo  49842  isinito2lem  49857  arweuthinc  49888  arweutermc  49889  discsntermlem  49929  basrestermcfolem  49930