Theorem eqeq1 2734

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq1i  2735  eqtr  2750  eqtr2  2751  iseqsetvlem  2793  eqsb1  2855  cbvexeqsetf  3465  cgsex4gOLD  3498  sbhypfOLD  3514  rexraleqim  3616  eqvincf  3619  pm13.183  3635  moeq  3681  mob  3691  euind  3698  reu2eqd  3710  reuind  3727  eqsbc1  3803  sbceqal  3818  csbhypf  3893  uniiunlem  4053  snjust  4591  elsng  4606  elprg  4615  reusngf  4641  rexreusng  4646  reuprg0  4669  rabrsn  4691  preq12bg  4820  intab  4945  uniintsn  4952  dfiun2g  4997  dfiin2g  4999  disji2  5094  disjprg  5106  unopab  5190  eusv1  5349  reusv2lem2  5357  reusv3  5363  opthg  5440  copsexgw  5453  copsexg  5454  propeqop  5470  euotd  5476  otiunsndisj  5483  elopabw  5489  solin  5576  elxpi  5663  opbrop  5739  relop  5817  ideqg  5818  dmopab2rex  5884  elrnmpt  5925  elrnmpt1  5927  elrnmptg  5928  restidsing  6027  somin1  6109  cnveqb  6172  reu3op  6268  reuop  6269  ordequn  6440  iotaval2  6482  funopg  6553  f0rn0  6748  fvelrnb  6924  fvmptg  6969  fndmin  7020  eldmrexrn  7066  foelrn  7082  foelrnf  7083  foco2  7084  fmptco  7104  funopsn  7123  funsndifnop  7126  fmptsng  7145  fmptsnd  7146  tpres  7178  eufnfv  7206  elabrex  7219  elabrexg  7220  abrexco  7221  f1veqaeq  7234  fpropnf1  7245  nf1const  7282  isosolem  7325  f1oiso  7329  eusvobj2  7382  oprabidw  7421  oprabid  7422  f1opr  7448  oprabv  7452  0mpo0  7475  elrnmpog  7527  elrnmpo  7528  elrnmpores  7530  ralrnmpo  7531  ov3  7555  ov6g  7556  ovelrn  7568  caovcang  7593  caovcan  7596  caofidlcan  7694  uniuni  7741  orduninsuc  7822  funcnvuni  7911  fiunlem  7923  fiun  7924  f1iun  7925  f1oweALT  7954  opiota  8041  eloprabi  8045  frxp  8108  funsssuppss  8172  dftpos4  8227  tz7.44-2  8378  tz7.44-3  8379  oev  8481  oalimcl  8527  omlimcl  8545  odi  8546  omeu  8552  oeeui  8569  nneob  8623  omopth  8629  eldifsucnn  8631  elqsg  8740  qsdisj  8770  qsel  8772  brecop  8786  eroveu  8788  erovlem  8789  elixpsn  8913  ixpsnf1o  8914  boxcutc  8917  2dom  9004  fundmen  9005  xpf1o  9109  nneneq  9176  fofinf1o  9290  elfi  9371  elfiun  9388  dffi3  9389  brwdom  9527  brwdom3  9542  unwdomg  9544  xpwdomg  9545  noinfep  9620  cantnfp1lem1  9638  cantnfp1lem3  9640  cantnflem1  9649  ssttrcl  9675  ttrclselem2  9686  scott0  9846  updjudhcoinrg  9893  updjud  9894  carden2a  9926  cardiun  9942  pm54.43lem  9960  alephval3  10070  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2b  10091  kmlem9  10119  kmlem12  10122  cardcf  10212  cfeq0  10216  cfsuc  10217  cff1  10218  cflim2  10223  cfss  10225  isfin5  10259  fin1a2lem11  10370  fin1a2lem13  10372  brdom7disj  10491  brdom6disj  10492  canthp1lem2  10613  canthp1  10614  tskuni  10743  gruina  10778  genpv  10959  genpelv  10960  addsrmo  11033  mulsrmo  11034  ltsosr  11054  ltresr  11100  axcnre  11124  axpre-lttri  11125  ltordlem  11710  ltord1  11711  fimaxre3  12136  supaddc  12157  supadd  12158  supmul1  12159  supmullem1  12160  supmullem2  12161  supmul  12162  creur  12187  creui  12188  nn1m1nn  12214  elz  12538  nn0ind-raph  12641  xnegeq  13174  xmullem2  13232  xmulasslem  13252  fleqceilz  13823  fseqsupubi  13950  sqeqor  14188  nn0opth2  14244  hash1snb  14391  hash2prde  14442  prprrab  14445  hash2pwpr  14448  tpf1ofv1  14469  tpf1ofv2  14470  tpfo  14472  fi1uzind  14479  wrd2ind  14695  cshfn  14762  cshf1  14782  2cshwcshw  14798  scshwfzeqfzo  14799  pfx2  14920  s3iunsndisj  14941  relexpsucnnr  14998  relexprelg  15011  rtrclreclem3  15033  shftfval  15043  sgnval  15061  01sqrexlem6  15220  reusq0  15438  summo  15690  fsum  15693  telfsumo  15775  infcvgaux1i  15830  infcvgaux2i  15831  mertenslem1  15857  mertenslem2  15858  mertens  15859  prodmo  15909  fprod  15914  ruclem12  16216  mod2eq1n2dvds  16324  divalg  16380  ndvdssub  16386  sadcp1  16432  smupp1  16457  gcdval  16473  bezoutlem1  16516  bezoutlem3  16518  bezoutlem4  16519  bezout  16520  lcmval  16569  coprmgcdb  16626  coprmdvds1  16629  divgcdcoprmex  16643  dvdsprime  16664  nprm  16665  dvdsprm  16680  coprm  16688  qnumval  16714  qdenval  16715  m1dvdsndvds  16776  reumodprminv  16782  pcval  16822  pceu  16824  pczpre  16825  pcdiv  16830  4sqlem2  16927  4sqlem4  16930  4sqlem12  16934  4sq  16942  vdwapval  16951  vdwapun  16952  vdwlem6  16964  cshwrepswhash1  17080  acsfn  17627  initoid  17970  termoid  17971  cat1lem  18065  posi  18285  gsumval2a  18619  smndex2dnrinv  18849  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2nmndlem5  18863  mgmnsgrpex  18865  sgrpnmndex  18866  cyccom  19142  ghmf1  19185  conjnmzb  19192  orbsta  19252  symgextfv  19355  symgextfo  19359  symgfixfo  19376  pmtrprfval  19424  pmtrprfvalrn  19425  psgneu  19443  psgnval  19444  psgnvali  19445  psgnvalii  19446  odfval  19469  odval  19471  dfod2  19501  submod  19506  isslw  19545  sylow2alem1  19554  sylow3lem2  19565  lsmelvalm  19588  lsmdisj2  19619  efgrelexlemb  19687  frgpup3lem  19714  cyggeninv  19820  gsumval3eu  19841  gsumval3lem2  19843  gsummpt1n0  19902  nn0gsumfz  19921  dprddisj2  19978  dpjrid  20001  pgpfac1lem3  20016  rrgeq0i  20615  domneq0  20624  domnlcanb  20636  domnrcanb  20638  abveq0  20734  abvtrivd  20748  lss1d  20876  lspsn  20915  ellspsn  20916  lspprel  21008  prmirredlem  21389  znf1o  21468  znfld  21477  znunit  21480  cygznlem3  21486  psgndif  21518  ipeq0  21554  obsip  21637  frlmphl  21697  uvcvval  21702  ellspd  21718  psrlidm  21878  psrridm  21879  psrascl  21895  mvrval2  21899  mvrf1  21902  mplmonmul  21950  evlslem3  21994  mhpsclcl  22041  psdmplcl  22056  psdmul  22060  psdmvr  22063  coe1tm  22166  coe1tmfv2  22168  cply1coe0  22195  cply1coe0bi  22196  gsummoncoe1  22202  mamufacex  22290  mat1comp  22334  mat1dimelbas  22365  mat1dimid  22368  scmatel  22399  scmateALT  22406  mavmulsolcl  22445  marrepeval  22457  marepveval  22462  mdetunilem8  22513  maducoeval2  22534  madugsum  22537  minmar1eval  22543  symgmatr01lem  22547  symgmatr01  22548  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  m2cpm  22635  m2cpminvid2lem  22648  decpmatid  22664  monmatcollpw  22673  pmatcollpw3fi1lem1  22680  mp2pm2mplem4  22703  fvmptnn04ifc  22746  chfacffsupp  22750  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulgsum  22758  cpmadumatpoly  22777  cayleyhamilton  22784  cayleyhamiltonALT  22785  istopon  22806  toponsspwpw  22816  fctop  22898  cctop  22900  ppttop  22901  pptbas  22902  epttop  22903  t0sep  23218  t1sep2  23263  cmpsublem  23293  cmpsub  23294  unisngl  23421  txuni2  23459  elpt  23466  ptbasfi  23475  xkoopn  23483  ptpjopn  23506  ptclsg  23509  dfac14lem  23511  ptcnp  23516  ptrescn  23533  tx1stc  23544  qtopeu  23610  kqt0lem  23630  isr0  23631  hauspwpwf1  23881  xmeteq0  24233  imasf1oxmet  24270  comet  24408  stdbdxmet  24410  met2ndci  24417  prdsxmslem2  24424  nrmmetd  24469  tngngp  24549  tngngp3  24551  xrsxmet  24705  iccpnfcnv  24849  iccpnfhmeo  24850  cnheibor  24861  elovolm  25383  ovolgelb  25388  ovolicc1  25424  ovolicc  25431  ioorval  25482  uniioombllem6  25496  dyadmax  25506  dyadmbl  25508  i1fadd  25603  i1fmul  25604  itg1addlem3  25606  i1fmulc  25611  itg2l  25637  itg2leub  25642  limcmpt  25791  limcco  25801  dvcobr  25856  dvcobrOLD  25857  deg1ldg  26004  ig1pval  26088  elply  26107  elply2  26108  coeval  26135  coe1termlem  26170  coe1term  26171  quotval  26207  plydivlem4  26211  plydivex  26212  vieta1  26227  aannenlem2  26244  aalioulem2  26248  abelthlem9  26357  logtayllem  26575  logtayl  26576  isosctrlem2  26736  leibpilem2  26858  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  mpodvdsmulf1o  27111  dvdsmulf1o  27113  perfectlem2  27148  lgsfval  27220  lgsval2lem  27225  lgsqrmodndvds  27271  lgsdchrval  27272  gausslemma2dlem0i  27282  2lgslem1b  27310  2lgslem3  27322  2sqlem2  27336  2sqlem8  27344  2sqlem9  27345  2sqlem11  27347  addsq2reu  27358  dchrisum0flblem1  27426  padicval  27535  padicabv  27548  ostth1  27551  sltval2  27575  sltintdifex  27580  sltres  27581  nolt02o  27614  madef  27771  addsval2  27877  addsproplem2  27884  addsproplem4  27886  addsproplem5  27887  addsproplem6  27888  addsprop  27890  addscut  27892  sleadd1  27903  addsuniflem  27915  addsunif  27916  addsasslem1  27917  addsasslem2  27918  addsbdaylem  27930  negsprop  27948  negsid  27954  mulsval2lem  28020  mulsproplem9  28034  mulsproplem12  28037  mulsprop  28040  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  mulsunif2  28080  precsexlemcbv  28115  precsexlem9  28124  precsexlem11  28126  n0s0suc  28241  onsfi  28254  n0s0m1  28259  nn1m1nns  28270  eucliddivs  28272  n0seo  28314  zseo  28315  expsval  28318  elzs12  28344  zs12ge0  28349  recut  28354  0reno  28355  renegscl  28356  readdscl  28357  remulscllem1  28358  remulscl  28360  axtgcgrid  28397  axtgbtwnid  28400  islmib  28721  inaghl  28779  axpaschlem  28874  axlowdimlem15  28890  axlowdim  28895  upgredg2vtx  29075  edglnl  29077  umgredgnlp  29081  usgredg2vtxeuALT  29156  uspgredg2v  29158  ushgredgedgloop  29165  nbusgredgeu  29300  cusgrfilem2  29391  cusgrfi  29393  vtxdushgrfvedg  29425  1loopgrvd2  29438  rusgr1vtxlem  29522  wlkeq  29569  wlkp1lem8  29615  upgrwlkdvdelem  29673  crctcshwlkn0lem6  29752  wlknwwlksnbij  29825  rusgrnumwwlkl1  29905  clwlkclwwlklem2a1  29928  clwwlknscsh  29998  eleclclwwlkn  30012  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknon1sn  30036  frgr3vlem1  30209  3vfriswmgrlem  30213  frgrncvvdeqlem3  30237  wlkl0  30303  frgrreggt1  30329  nvz  30605  nmosetn0  30701  nmoolb  30707  nmoubi  30708  nmlno0lem  30729  nmlno0i  30730  hvsubeq0  31004  hvaddcan  31006  normsub0  31072  norm1exi  31186  pjhval  31333  omlsii  31339  omlsi  31340  pjoml  31372  h1de2ci  31492  spansneleq  31506  h1datomi  31517  h1datom  31518  spansncv  31589  5oalem6  31595  pj11  31650  nmopsetn0  31801  nmfnsetn0  31814  nmoplb  31843  nmopub  31844  nmfnlb  31860  nmfnleub  31861  nmlnop0iALT  31931  nmlnop0  31934  lnopeq  31945  nmopun  31950  nmcexi  31962  branmfn  32041  pjnmopi  32084  pj3i  32144  atss  32282  atom1d  32289  chirred  32331  cdj3lem2  32371  eqelbid  32411  elabreximd  32446  disjxpin  32524  disjunsn  32530  br8d  32545  fmptcof2  32588  sgn3da  32766  sgnmul  32767  sgnnbi  32770  sgnpbi  32771  sgn0bi  32772  psgnfzto1stlem  33064  sgnsval  33125  elrgspnlem2  33201  elrgspnlem3  33202  domnlcanOLD  33237  linds2eq  33359  elrspunsn  33407  mxidlmax  33443  1arithidomlem1  33513  1arithidom  33515  1arithufdlem1  33522  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  1arithufd  33526  dfufd2  33528  ply1dg1rt  33555  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  rtelextdg2lem  33723  constrsuc  33735  constrcbvlem  33752  2sqr3minply  33777  madjusmdetlem2  33825  madjusmdet  33828  zarclssn  33870  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iifhom  33934  xrge0tmd  33942  xrge0tmdALT  33943  esumc  34048  plymulx0  34545  signspval  34550  tgoldbachgt  34661  bnj1468  34843  f1resfz0f1d  35108  acycgrcycl  35141  sconnpi1  35233  cvmlift3lem2  35314  satfv0  35352  satfv1  35357  satfbrsuc  35360  satfrnmapom  35364  satfv0fun  35365  satf0op  35371  sat1el2xp  35373  fmlafvel  35379  fmla1  35381  isfmlasuc  35382  fmlaomn0  35384  gonan0  35386  goaln0  35387  gonar  35389  goalr  35391  fmla0disjsuc  35392  fmlasucdisj  35393  satffunlem1lem1  35396  satffunlem2lem1  35398  dmopab3rexdif  35399  satfv0fvfmla0  35407  sategoelfvb  35413  ex-sategoelel  35415  satfv1fvfmla1  35417  2goelgoanfmla1  35418  ex-sategoelelomsuc  35420  ex-sategoelel12  35421  prv1n  35425  ellcsrspsn  35635  r1peuqusdeg1  35637  br8  35750  br6  35751  br4  35752  rdgprc0  35788  dfrdg2  35790  dfbigcup2  35894  elsingles  35913  dfiota3  35918  brimageg  35922  brdomaing  35930  brrangeg  35931  dfrdg4  35946  elaltxp  35970  funtransport  36026  fvtransport  36027  brsegle  36103  funray  36135  fvray  36136  funline  36137  fvline  36139  ellines  36147  linethru  36148  rankeq1o  36166  subtr  36309  subtr2  36310  nn0prpw  36318  bj-elabd2ALT  36920  bj-gabss  36930  bj-imafv  37246  topdifinffinlem  37342  topdifinffin  37343  topdifinfeq  37345  finxpreclem2  37385  finxpreclem3  37388  fvineqsnf1  37405  fvineqsneu  37406  wl-ax12v2cl  37501  wl-issetft  37577  fin2so  37608  ptrest  37620  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  ftc1anc  37702  unirep  37715  sdclem2  37743  sdclem1  37744  sdc  37745  fdc  37746  isbnd  37781  heibor1lem  37810  heiborlem4  37815  heiborlem6  37817  heiborlem10  37821  ismgmOLD  37851  maxidlmax  38044  prnc  38068  isfldidl  38069  dmnnzd  38076  disjressuc2  38381  qsdisjALTV  38613  eqvrelqsel  38614  riotasvd  38956  lshpdisj  38987  lsat0cv  39033  lcvexchlem4  39037  lcvexchlem5  39038  lshpkrlem1  39110  lshpkrlem2  39111  lshpkrlem3  39112  lshpkrcl  39116  islshpkrN  39120  atnle  39317  glbconxN  39379  isline  39740  ispointN  39743  pmapglbx  39770  ispsubcl2N  39948  lhp2atnle  40034  cdleme43fsv1snlem  40421  cdleme40v  40470  cdlemkid5  40936  cdlemkid  40937  dvhb1dimN  40987  dib1dim  41166  dicopelval  41178  dicelval1sta  41188  diclspsn  41195  dihvalcqpre  41236  dihglblem2aN  41294  dihglblem2N  41295  dih1dimatlem  41330  dihpN  41337  dochfl1  41477  lcfl7N  41502  lcf1o  41552  hvmapvalvalN  41762  hdmapval2lem  41832  aks6d1c1  42111  aks6d1c4  42119  sticksstones10  42150  sticksstones12a  42152  aks6d1c7  42179  sn-iotalem  42216  f1o2d2  42228  fiabv  42531  evlsbagval  42561  selvvvval  42580  fsuppind  42585  absnw  42673  elrfi  42689  nacsfg  42700  mzpcompact2lem  42746  eldioph2b  42758  eldioph3  42761  eldiophss  42769  diophrex  42770  elnn0rabdioph  42798  rencldnfilem  42815  elpell1qr  42842  elpell14qr  42844  elpell1234qr  42846  jm2.27  43004  rmydioph  43010  expdiophlem2  43018  wepwsolem  43038  aomclem6  43055  lnr2i  43112  lpirlnr  43113  hbtlem2  43120  hbtlem4  43122  hbtlem5  43124  rngunsnply  43165  flcidc  43166  onsucelab  43259  limnsuc  43261  nnoeomeqom  43308  cantnfresb  43320  tfsconcatfv2  43336  tfsconcatb0  43340  oaun3lem1  43370  oadif1lem  43375  oadif1  43376  clcnvlem  43619  brtrclfv2  43723  frege55lem1c  43912  frege104  43963  clsk1indlem0  44037  clsk1indlem2  44038  clsk1indlem3  44039  clsk1indlem4  44040  clsk1indlem1  44041  pm13.192  44406  equncomVD  44864  csbingVD  44880  csbsngVD  44889  csbfv12gALTVD  44895  relopabVD  44897  refsum2cnlem1  45038  elrnmptf  45182  upbdrech  45310  ssfiunibd  45314  iccshift  45523  iooshift  45527  fsumf1of  45579  limcperiod  45633  climinf2mpt  45719  climinfmpt  45720  cncfshiftioo  45897  itgiccshift  45985  itgperiod  45986  stoweidlem46  46051  fourierdlem29  46141  fourierdlem37  46149  fourierdlem48  46159  fourierdlem51  46162  fourierdlem54  46165  fourierdlem62  46173  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem92  46203  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem103  46214  fourierdlem104  46215  fourierdlem105  46216  fourierdlem108  46219  fourierdlem110  46221  fourierdlem112  46223  etransclem1  46240  etransclem5  46244  etransclem17  46256  etransclem32  46271  etransclem41  46280  sge0f1o  46387  sge0resplit  46411  sge0fodjrnlem  46421  nnfoctbdjlem  46460  nnfoctbdj  46461  ovnval  46546  ovnlecvr  46563  ovnpnfelsup  46564  ovn0lem  46570  hoidmvval  46582  hoidmvlelem1  46600  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  hoidifhspval3  46624  hspmbllem2  46632  hoimbl  46636  ovnsubadd2  46651  ovolval5lem2  46658  ovolval5lem3  46659  ovolval5  46660  ovnovol  46664  fsetsnf  47056  fsetsnfo  47058  fcoresf1  47074  aiotaval  47100  euoreqb  47114  afv0fv0  47154  afvfv0bi  47157  afvelrnb  47168  afvelrnb0  47169  afv20defat  47237  otiunsndisjX  47284  fun2dmnopgexmpl  47289  2ffzoeq  47332  modmkpkne  47366  elsetpreimafvb  47389  imasetpreimafvbijlemfo  47410  fargshiftf1  47446  fargshiftfo  47447  ichnreuop  47477  ichreuopeq  47478  elsprel  47480  spr0nelg  47481  sprel  47489  prelspr  47491  sprsymrelf1lem  47496  sprsymrelfolem2  47498  paireqne  47516  prprelb  47521  prprelprb  47522  reupr  47527  reuopreuprim  47531  fmtnoprmfac1lem  47569  fmtnofac2  47574  m1expevenALTV  47652  odd2np1ALTV  47679  opoeALTV  47688  opeoALTV  47689  perfectALTVlem2  47727  isgbe  47756  isgbow  47757  isgbo  47758  sbgoldbalt  47786  sgoldbeven3prm  47788  mogoldbb  47790  nnsum3primesgbe  47797  nnsum3primesle9  47799  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  vopnbgrel  47858  dfclnbgr6  47860  dfnbgr6  47861  isuspgrim0  47898  isuspgrimlem  47899  clnbgrgrim  47938  usgrgrtrirex  47953  stgredgel  47960  stgrusgra  47962  stgr1  47964  grlimgrtri  47999  gpgiedgdmel  48044  gpgedgel  48045  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem4  48113  pgnbgreunbgr  48119  uspgrsprf1  48139  uspgrsprfo  48140  0nodd  48162  1odd  48163  2nodd  48164  0even  48229  1neven  48230  2even  48231  2zlidl  48232  2zrngamgm  48237  2zrngagrp  48241  2zrngmmgm  48244  2zrngnmrid  48248  suppmptcfin  48368  lcoval  48405  linc0scn0  48416  linc1  48418  el0ldep  48459  snlindsntor  48464  blenval  48564  nn0sumshdiglemB  48613  itcoval1  48656  mo0  48806  eloprab1st2nd  48860  oppcmndclem  49010  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033  upciclem1  49159  oppcup3lem  49199  isthincd2lem1  49418  termcbasmo  49476  isinito2lem  49491  arweuthinc  49522  arweutermc  49523  discsntermlem  49563  basrestermcfolem  49564