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  3445  rexraleqim  3590  eqvincf  3593  pm13.183  3609  moeq  3654  mob  3664  euind  3671  reu2eqd  3683  reuind  3700  eqsbc1  3776  sbceqal  3791  csbhypf  3866  uniiunlem  4028  snjust  4567  elsng  4582  elprg  4591  reusngf  4619  rexreusng  4624  reuprg0  4647  rabrsn  4669  preq12bg  4797  intab  4921  uniintsn  4928  dfiun2g  4973  dfiin2g  4974  disji2  5070  disjprg  5082  unopab  5166  eusv1  5329  reusv2lem2  5337  reusv3  5343  axprg  5375  opthg  5426  copsexgw  5439  copsexg  5440  propeqop  5456  euotd  5462  otiunsndisj  5469  elopabw  5475  solin  5560  elxpi  5647  opbrop  5723  relop  5800  ideqg  5801  dmopab2rex  5867  elrnmpt  5908  elrnmpt1  5910  elrnmptg  5911  restidsing  6013  somin1  6091  cnveqb  6155  reu3op  6251  reuop  6252  ordequn  6423  iotaval2  6464  funopg  6527  f0rn0  6720  fvelrnb  6895  fvmptg  6940  fndmin  6992  eldmrexrn  7038  foelrn  7054  foelrnf  7055  foco2  7056  fmptco  7077  funopsn  7096  funsndifnop  7099  fmptsng  7117  fmptsnd  7118  tpres  7150  eufnfv  7178  elabrex  7191  elabrexg  7192  abrexco  7193  f1veqaeq  7205  fpropnf1  7216  nf1const  7253  isosolem  7296  f1oiso  7300  eusvobj2  7353  oprabidw  7392  oprabid  7393  f1opr  7417  oprabv  7421  0mpo0  7444  elrnmpog  7496  elrnmpo  7497  elrnmpores  7499  ralrnmpo  7500  ov3  7524  ov6g  7525  ovelrn  7537  caovcang  7562  caovcan  7565  caofidlcan  7663  uniuni  7710  orduninsuc  7788  funcnvuni  7877  fiunlem  7889  fiun  7890  f1iun  7891  f1oweALT  7919  opiota  8006  eloprabi  8010  frxp  8070  funsssuppss  8134  dftpos4  8189  tz7.44-2  8340  tz7.44-3  8341  oev  8443  oalimcl  8489  omlimcl  8507  odi  8508  omeu  8514  oeeui  8532  nneob  8586  omopth  8592  eldifsucnn  8594  elqsg  8704  qsdisj  8735  qsel  8737  brecop  8751  eroveu  8753  erovlem  8754  elixpsn  8879  ixpsnf1o  8880  boxcutc  8883  2dom  8971  fundmen  8972  xpf1o  9071  nneneq  9134  fofinf1o  9236  elfi  9320  elfiun  9337  dffi3  9338  brwdom  9476  brwdom3  9491  unwdomg  9493  xpwdomg  9494  noinfep  9575  cantnfp1lem1  9593  cantnfp1lem3  9595  cantnflem1  9604  ssttrcl  9630  ttrclselem2  9641  scott0  9804  updjudhcoinrg  9851  updjud  9852  carden2a  9884  cardiun  9900  pm54.43lem  9918  alephval3  10026  dfac5lem3  10041  dfac5lem4  10042  dfac5lem4OLD  10044  dfac2b  10047  kmlem9  10075  kmlem12  10078  cardcf  10168  cfeq0  10172  cfsuc  10173  cff1  10174  cflim2  10179  cfss  10181  isfin5  10215  fin1a2lem11  10326  fin1a2lem13  10328  brdom7disj  10447  brdom6disj  10448  canthp1lem2  10570  canthp1  10571  tskuni  10700  gruina  10735  genpv  10916  genpelv  10917  addsrmo  10990  mulsrmo  10991  ltsosr  11011  ltresr  11057  axcnre  11081  axpre-lttri  11082  ltordlem  11669  ltord1  11670  fimaxre3  12096  supaddc  12117  supadd  12118  supmul1  12119  supmullem1  12120  supmullem2  12121  supmul  12122  creur  12147  creui  12148  nn1m1nn  12189  elz  12520  nn0ind-raph  12623  xnegeq  13153  xmullem2  13211  xmulasslem  13231  fleqceilz  13807  fseqsupubi  13934  sqeqor  14172  nn0opth2  14228  hash1snb  14375  hash2prde  14426  prprrab  14429  hash2pwpr  14432  tpf1ofv1  14453  tpf1ofv2  14454  tpfo  14456  fi1uzind  14463  wrd2ind  14679  cshfn  14746  cshf1  14766  2cshwcshw  14781  scshwfzeqfzo  14782  pfx2  14903  s3iunsndisj  14924  relexpsucnnr  14981  relexprelg  14994  rtrclreclem3  15016  shftfval  15026  sgnval  15044  01sqrexlem6  15203  reusq0  15421  summo  15673  fsum  15676  telfsumo  15759  infcvgaux1i  15816  infcvgaux2i  15817  mertenslem1  15843  mertenslem2  15844  mertens  15845  prodmo  15895  fprod  15900  ruclem12  16202  mod2eq1n2dvds  16310  divalg  16366  ndvdssub  16372  sadcp1  16418  smupp1  16443  gcdval  16459  bezoutlem1  16502  bezoutlem3  16504  bezoutlem4  16505  bezout  16506  lcmval  16555  coprmgcdb  16612  coprmdvds1  16615  divgcdcoprmex  16629  dvdsprime  16650  nprm  16651  dvdsprm  16667  coprm  16675  qnumval  16701  qdenval  16702  m1dvdsndvds  16763  reumodprminv  16769  pcval  16809  pceu  16811  pczpre  16812  pcdiv  16817  4sqlem2  16914  4sqlem4  16917  4sqlem12  16921  4sq  16929  vdwapval  16938  vdwapun  16939  vdwlem6  16951  cshwrepswhash1  17067  acsfn  17619  initoid  17962  termoid  17963  cat1lem  18057  posi  18277  gsumval2a  18647  smndex2dnrinv  18880  mgm2nsgrplem2  18884  mgm2nsgrplem3  18885  sgrp2nmndlem5  18894  mgmnsgrpex  18896  sgrpnmndex  18897  cyccom  19172  ghmf1  19215  conjnmzb  19222  orbsta  19282  symgextfv  19387  symgextfo  19391  symgfixfo  19408  pmtrprfval  19456  pmtrprfvalrn  19457  psgneu  19475  psgnval  19476  psgnvali  19477  psgnvalii  19478  odfval  19501  odval  19503  dfod2  19533  submod  19538  isslw  19577  sylow2alem1  19586  sylow3lem2  19597  lsmelvalm  19620  lsmdisj2  19651  efgrelexlemb  19719  frgpup3lem  19746  cyggeninv  19852  gsumval3eu  19873  gsumval3lem2  19875  gsummpt1n0  19934  nn0gsumfz  19953  dprddisj2  20010  dpjrid  20033  pgpfac1lem3  20048  rrgeq0i  20670  domneq0  20679  domnlcanb  20691  domnrcanb  20693  abveq0  20789  abvtrivd  20803  lss1d  20952  lspsn  20991  ellspsn  20992  lspprel  21084  prmirredlem  21465  znf1o  21544  znfld  21553  znunit  21556  cygznlem3  21562  psgndif  21595  ipeq0  21631  obsip  21714  frlmphl  21774  uvcvval  21779  ellspd  21795  psrlidm  21953  psrridm  21954  psrascl  21970  mvrval2  21974  mvrf1  21977  mplmonmul  22027  evlslem3  22071  mhpsclcl  22126  psdmplcl  22141  psdmul  22145  psdmvr  22148  coe1tm  22251  coe1tmfv2  22253  cply1coe0  22279  cply1coe0bi  22280  gsummoncoe1  22286  mamufacex  22374  mat1comp  22418  mat1dimelbas  22449  mat1dimid  22452  scmatel  22483  scmateALT  22490  mavmulsolcl  22529  marrepeval  22541  marepveval  22546  mdetunilem8  22597  maducoeval2  22618  madugsum  22621  minmar1eval  22627  symgmatr01lem  22631  symgmatr01  22632  gsummatr01lem3  22635  gsummatr01lem4  22636  gsummatr01  22637  m2cpm  22719  m2cpminvid2lem  22732  decpmatid  22748  monmatcollpw  22757  pmatcollpw3fi1lem1  22764  mp2pm2mplem4  22787  fvmptnn04ifc  22830  chfacffsupp  22834  chfacfscmul0  22836  chfacfscmulgsum  22838  chfacfpmmul0  22840  chfacfpmmulgsum  22842  cpmadumatpoly  22861  cayleyhamilton  22868  cayleyhamiltonALT  22869  istopon  22890  toponsspwpw  22900  fctop  22982  cctop  22984  ppttop  22985  pptbas  22986  epttop  22987  t0sep  23302  t1sep2  23347  cmpsublem  23377  cmpsub  23378  unisngl  23505  txuni2  23543  elpt  23550  ptbasfi  23559  xkoopn  23567  ptpjopn  23590  ptclsg  23593  dfac14lem  23595  ptcnp  23600  ptrescn  23617  tx1stc  23628  qtopeu  23694  kqt0lem  23714  isr0  23715  hauspwpwf1  23965  xmeteq0  24316  imasf1oxmet  24353  comet  24491  stdbdxmet  24493  met2ndci  24500  prdsxmslem2  24507  nrmmetd  24552  tngngp  24632  tngngp3  24634  xrsxmet  24788  iccpnfcnv  24924  iccpnfhmeo  24925  cnheibor  24935  elovolm  25455  ovolgelb  25460  ovolicc1  25496  ovolicc  25503  ioorval  25554  uniioombllem6  25568  dyadmax  25578  dyadmbl  25580  i1fadd  25675  i1fmul  25676  itg1addlem3  25678  i1fmulc  25683  itg2l  25709  itg2leub  25714  limcmpt  25863  limcco  25873  dvcobr  25926  deg1ldg  26070  ig1pval  26154  elply  26173  elply2  26174  coeval  26201  coe1termlem  26236  coe1term  26237  quotval  26272  plydivlem4  26276  plydivex  26277  vieta1  26292  aannenlem2  26309  aalioulem2  26313  abelthlem9  26421  logtayllem  26639  logtayl  26640  isosctrlem2  26799  leibpilem2  26921  rlimcnp2  26946  efrlim  26949  efrlimOLD  26950  mpodvdsmulf1o  27174  dvdsmulf1o  27176  perfectlem2  27210  lgsfval  27282  lgsval2lem  27287  lgsqrmodndvds  27333  lgsdchrval  27334  gausslemma2dlem0i  27344  2lgslem1b  27372  2lgslem3  27384  2sqlem2  27398  2sqlem8  27406  2sqlem9  27407  2sqlem11  27409  addsq2reu  27420  dchrisum0flblem1  27488  padicval  27597  padicabv  27610  ostth1  27613  ltsval2  27637  ltsintdifex  27642  ltsres  27643  nolt02o  27676  madef  27845  addsval2  27972  addsproplem2  27979  addsproplem4  27981  addsproplem5  27982  addsproplem6  27983  addsprop  27985  addcuts  27987  leadds1  27998  addsuniflem  28010  addsunif  28011  addsasslem1  28012  addsasslem2  28013  addbdaylem  28026  negsprop  28044  negsid  28050  mulsval2lem  28119  mulsproplem9  28133  mulsproplem12  28136  mulsprop  28139  sltmuls1  28156  sltmuls2  28157  mulsuniflem  28158  addsdilem1  28160  addsdilem2  28161  mulsasslem1  28172  mulsasslem2  28173  mulsunif2  28179  precsexlemcbv  28215  precsexlem9  28224  precsexlem11  28226  n0s0suc  28351  onsfi  28365  n0s0m1  28371  nn1m1nns  28383  eucliddivs  28385  n0seo  28430  zseo  28431  expsval  28434  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  bdayfinbnd  28478  elz12s  28481  z12zsodd  28491  z12sge0  28492  recut  28503  elreno2  28504  renegscl  28507  readdscl  28508  remulscllem1  28509  remulscl  28511  axtgcgrid  28548  axtgbtwnid  28551  islmib  28872  inaghl  28930  axpaschlem  29026  axlowdimlem15  29042  axlowdim  29047  upgredg2vtx  29227  edglnl  29229  umgredgnlp  29233  usgredg2vtxeuALT  29308  uspgredg2v  29310  ushgredgedgloop  29317  nbusgredgeu  29452  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  32676  disjunsn  32682  br8d  32699  fmptcof2  32748  sgn3da  32925  sgnmul  32926  sgnnbi  32929  sgnpbi  32930  sgn0bi  32931  psgnfzto1stlem  33179  sgnsval  33240  elrgspnlem2  33322  elrgspnlem3  33323  domnlcanOLD  33359  linds2eq  33459  elrspunsn  33507  mxidlmax  33543  1arithidomlem1  33613  1arithidom  33615  1arithufdlem1  33622  1arithufdlem2  33623  1arithufdlem3  33624  1arithufdlem4  33625  1arithufd  33626  dfufd2  33628  ply1dg1rt  33658  mplvrpmrhm  33709  psrmonmul  33712  esplyfvaln  33736  lbsdiflsp0  33789  fedgmullem1  33792  fedgmullem2  33793  rtelextdg2lem  33889  constrsuc  33901  constrcbvlem  33918  2sqr3minply  33943  madjusmdetlem2  33991  madjusmdet  33994  zarclssn  34036  xrge0iifcnv  34096  xrge0iifcv  34097  xrge0iifhom  34100  xrge0tmd  34108  xrge0tmdALT  34109  esumc  34214  plymulx0  34710  signspval  34715  tgoldbachgt  34826  bnj1468  35007  fineqvnttrclselem3  35286  fineqvnttrclse  35287  f1resfz0f1d  35315  acycgrcycl  35348  sconnpi1  35440  cvmlift3lem2  35521  satfv0  35559  satfv1  35564  satfbrsuc  35567  satfrnmapom  35571  satfv0fun  35572  satf0op  35578  sat1el2xp  35580  fmlafvel  35586  fmla1  35588  isfmlasuc  35589  fmlaomn0  35591  gonan0  35593  goaln0  35594  gonar  35596  goalr  35598  fmla0disjsuc  35599  fmlasucdisj  35600  satffunlem1lem1  35603  satffunlem2lem1  35605  dmopab3rexdif  35606  satfv0fvfmla0  35614  sategoelfvb  35620  ex-sategoelel  35622  satfv1fvfmla1  35624  2goelgoanfmla1  35625  ex-sategoelelomsuc  35627  ex-sategoelel12  35628  prv1n  35632  ellcsrspsn  35842  r1peuqusdeg1  35844  br8  35957  br6  35958  br4  35959  rdgprc0  35992  dfrdg2  35994  dfbigcup2  36098  elsingles  36117  dfiota3  36122  brimageg  36126  brdomaing  36134  brrangeg  36135  dfrdg4  36152  elaltxp  36176  funtransport  36232  fvtransport  36233  brsegle  36309  funray  36341  fvray  36342  funline  36343  fvline  36345  ellines  36353  linethru  36354  rankeq1o  36372  subtr  36515  subtr2  36516  nn0prpw  36524  bj-elabd2ALT  37251  bj-gabss  37261  bj-imafv  37584  topdifinffinlem  37680  topdifinffin  37681  topdifinfeq  37683  finxpreclem2  37723  finxpreclem3  37726  fvineqsnf1  37743  fvineqsneu  37744  wl-ax12v2cl  37839  wl-dfclel  37848  wl-issetft  37924  fin2so  37945  ptrest  37957  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  poimirlem28  37986  poimirlem31  37989  poimirlem32  37990  heicant  37993  mblfinlem2  37996  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  ftc1anc  38039  unirep  38052  sdclem2  38080  sdclem1  38081  sdc  38082  fdc  38083  isbnd  38118  heibor1lem  38147  heiborlem4  38152  heiborlem6  38154  heiborlem10  38158  ismgmOLD  38188  maxidlmax  38381  prnc  38405  isfldidl  38406  dmnnzd  38413  disjressuc2  38749  qsdisjALTV  39037  eqvrelqsel  39038  riotasvd  39419  lshpdisj  39450  lsat0cv  39496  lcvexchlem4  39500  lcvexchlem5  39501  lshpkrlem1  39573  lshpkrlem2  39574  lshpkrlem3  39575  lshpkrcl  39579  islshpkrN  39583  atnle  39780  glbconxN  39841  isline  40202  ispointN  40205  pmapglbx  40232  ispsubcl2N  40410  lhp2atnle  40496  cdleme43fsv1snlem  40883  cdleme40v  40932  cdlemkid5  41398  cdlemkid  41399  dvhb1dimN  41449  dib1dim  41628  dicopelval  41640  dicelval1sta  41650  diclspsn  41657  dihvalcqpre  41698  dihglblem2aN  41756  dihglblem2N  41757  dih1dimatlem  41792  dihpN  41799  dochfl1  41939  lcfl7N  41964  lcf1o  42014  hvmapvalvalN  42224  hdmapval2lem  42294  aks6d1c1  42572  aks6d1c4  42580  sticksstones10  42611  sticksstones12a  42613  aks6d1c7  42640  sn-iotalem  42679  f1o2d2  42691  fiabv  42998  evlsbagval  43019  selvvvval  43035  fsuppind  43040  absnw  43128  elrfi  43143  nacsfg  43154  mzpcompact2lem  43200  eldioph2b  43212  eldioph3  43215  eldiophss  43223  diophrex  43224  elnn0rabdioph  43252  rencldnfilem  43269  elpell1qr  43296  elpell14qr  43298  elpell1234qr  43300  jm2.27  43457  rmydioph  43463  expdiophlem2  43471  wepwsolem  43491  aomclem6  43508  lnr2i  43565  lpirlnr  43566  hbtlem2  43573  hbtlem4  43575  hbtlem5  43577  rngunsnply  43618  flcidc  43619  onsucelab  43712  limnsuc  43714  nnoeomeqom  43761  cantnfresb  43773  tfsconcatfv2  43789  tfsconcatb0  43793  oaun3lem1  43823  oadif1lem  43828  oadif1  43829  clcnvlem  44071  brtrclfv2  44175  frege55lem1c  44364  frege104  44415  clsk1indlem0  44489  clsk1indlem2  44490  clsk1indlem3  44491  clsk1indlem4  44492  clsk1indlem1  44493  pm13.192  44858  equncomVD  45315  csbingVD  45331  csbsngVD  45340  csbfv12gALTVD  45346  relopabVD  45348  refsum2cnlem1  45489  elrnmptf  45632  upbdrech  45759  ssfiunibd  45763  iccshift  45969  iooshift  45973  fsumf1of  46025  limcperiod  46079  climinf2mpt  46163  climinfmpt  46164  cncfshiftioo  46341  itgiccshift  46429  itgperiod  46430  stoweidlem46  46495  fourierdlem29  46585  fourierdlem37  46593  fourierdlem48  46603  fourierdlem51  46606  fourierdlem54  46609  fourierdlem62  46617  fourierdlem79  46634  fourierdlem81  46636  fourierdlem82  46637  fourierdlem92  46647  fourierdlem96  46651  fourierdlem97  46652  fourierdlem98  46653  fourierdlem99  46654  fourierdlem103  46658  fourierdlem104  46659  fourierdlem105  46660  fourierdlem108  46663  fourierdlem110  46665  fourierdlem112  46667  etransclem1  46684  etransclem5  46688  etransclem17  46700  etransclem32  46715  etransclem41  46724  sge0f1o  46831  sge0resplit  46855  sge0fodjrnlem  46865  nnfoctbdjlem  46904  nnfoctbdj  46905  ovnval  46990  ovnlecvr  47007  ovnpnfelsup  47008  ovn0lem  47014  hoidmvval  47026  hoidmvlelem1  47044  ovnhoilem1  47050  ovnhoi  47052  ovnlecvr2  47059  hoidifhspval3  47068  hspmbllem2  47076  hoimbl  47080  ovnsubadd2  47095  ovolval5lem2  47102  ovolval5lem3  47103  ovolval5  47104  ovnovol  47108  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