Theorem eqeq12d 2750

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)

Hypotheses

Ref	Expression
eqeq12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eqeq12d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
3	1, 2	eqeqan12d 2748	. 2 ⊢ ((𝜑 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	anidms 566	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  neeq12d  2999  cdeqeq  3783  sbceqg  4417  csbun  4446  csbin  4447  csbdif  4529  csbif  4587  iununi  5103  csbopab  5564  csbopabgALT  5565  dfid2  5584  csbima12  6098  dmsnsnsn  6241  csbcog  6318  dfpred3g  6334  preddowncl  6354  limeq  6397  csbiota  6555  fveqres  6953  opabiota  6990  fvmptf  7036  eqfnfv2f  7054  fvreseq0  7057  fveqdmss  7097  fvcofneq  7112  fnressn  7177  fnelfp  7194  fprb  7213  fnprb  7227  fntpb  7228  f1cofveqaeqALT  7278  nvocnv  7300  cocan1  7310  cocan2  7311  2fvcoidd  7316  fliftfun  7331  weniso  7373  csbriota  7402  oveqrspc2v  7457  csbov123  7474  eqfnov  7561  ovmpos  7580  ov2gf  7581  ovmpodxf  7582  caovcomg  7627  caovassg  7630  caovcang  7633  caovcanrd  7635  caovcan  7636  caovdig  7646  caovdirg  7649  caovmo  7669  coof  7720  offveqb  7723  caofid0l  7729  caofid0r  7730  caofass  7735  caonncan  7739  ordunisuc  7851  onsucuni2  7853  orduninsuc  7863  op1stg  8024  op2ndg  8025  f1o2ndf1  8145  xpord2pred  8168  xpord3pred  8175  poseq  8181  soseq  8182  fnsuppres  8214  csbfrecsg  8307  fpr3g  8308  frrlem1  8309  frrlem12  8320  frrlem13  8321  fpr2a  8325  wfr3g  8345  wfrlem1OLD  8346  wfrlem3OLDa  8349  wfrlem12OLD  8358  wfrlem14OLD  8360  wfrlem15OLD  8361  wfr2aOLD  8364  onfununi  8379  tfrlem1  8414  tfrlem3a  8415  tfrlem5  8418  tfrlem9  8423  tfrlem11  8426  tfrlem12  8427  tfr3  8437  tz7.44-1  8444  tz7.44-2  8445  tz7.44-3  8446  rdglem1  8453  rdg0g  8465  seqomlem1  8488  oalim  8568  omlim  8569  oelim  8570  oa0r  8574  om0r  8575  om1r  8579  oaass  8597  oarec  8598  odi  8615  omass  8616  oelim2  8631  oeoalem  8632  oeoa  8633  oeoelem  8634  oeoe  8635  nna0r  8645  nnacom  8653  nnaass  8658  nndi  8659  nnmass  8660  nnmsucr  8661  nnmcom  8662  oaabs  8684  oaabs2  8685  omabs  8687  naddcllem  8712  naddcom  8718  naddrid  8719  naddass  8732  naddsuc2  8737  naddoa  8738  ecovcom  8861  ecovass  8862  ecovdi  8863  dom2lem  9030  unxpdomlem2  9284  unxpdomlem3  9285  ixpfi2  9387  fipreima  9395  ordiso2  9552  wemaplem1  9583  wemaplem2  9584  wemapsolem  9587  cantnfval2  9706  cantnfp1lem3  9717  oemapvali  9721  cantnflem1c  9724  cantnflem1  9726  wemapwe  9734  rnttrcl  9759  tcvalg  9775  frr3g  9793  frr2  9797  rankvalg  9854  rankonidlem  9865  ranklim  9881  rankuni  9900  updjud  9971  cardprclem  10016  cardprc  10017  carduni  10018  fseqenlem1  10061  fodomacn  10093  alephcard  10107  alephfp2  10146  alephval3  10147  dfac12lem1  10181  dfac12lem2  10182  dfac12r  10184  ackbij1lem8  10263  ackbij1lem14  10269  ackbij1lem16  10271  ackbij2lem3  10277  cardcf  10289  sornom  10314  fin23lem28  10377  isf32lem2  10391  itunitc  10458  ituniiun  10459  axdc3lem2  10488  axdc4lem  10492  ttukeylem3  10548  ttukey2g  10553  fpwwe2lem7  10674  fpwwecbv  10681  canth4  10684  pwfseqlem2  10696  addcanpi  10936  mulcanpi  10937  recrecnq  11004  ltexnq  11012  genpv  11036  0idsr  11134  1idsr  11135  ax1rid  11198  mulrid  11256  addcan  11442  addcan2  11443  mulcand  11893  mulcan2d  11894  mulcan2g  11914  div11OLD  11948  divmuleq  11969  conjmul  11981  eqneg  11984  ofsubeq0  12260  rpnnen1lem6  13021  cnref1o  13024  xmulasslem  13323  xmulass  13325  xadddi2  13335  prunioo  13517  fzsuc2  13618  fzprval  13621  fztpval  13622  fzosplitprm1  13812  modadd1  13944  modmul1  13961  addmodlteq  13983  om2uzsuci  13985  om2uzrdg  13993  uzrdgxfr  14004  seq1  14051  seqp1  14053  seqfveq2  14061  seqfveq  14063  seqshft2  14065  seqsplit  14072  seqcaopr3  14074  seqcaopr2  14075  seqf1olem2a  14077  seqf1olem2  14079  seqf1o  14080  seqid  14084  seqid2  14085  seqhomo  14086  ser1const  14095  seqof2  14097  mulexp  14138  expadd  14141  expmul  14144  binom2  14252  sq01  14260  modexp  14273  bcpasc  14356  hashgadd  14412  hashdom  14414  hashfzo  14464  hashfzp1  14466  hashxplem  14468  hashxp  14469  hashmap  14470  hashpw  14471  hashbclem  14487  hashbc  14488  hashfacen  14489  hashf1lem1  14490  hashf1lem2  14491  hashf1  14492  seqcoll  14499  eqs1  14646  swrdspsleq  14699  pfxeq  14730  pfxsuff1eqwrdeq  14733  ccatopth2  14751  cats1un  14755  swrdccatin1  14759  swrdccat3blem  14773  cshf1  14844  repswcshw  14846  s2eq2s1eq  14971  s3eqs2s1eq  14973  pfx2  14982  2swrd2eqwrdeq  14988  wwlktovf1  14992  eqwrds3  14996  relexpsucnnr  15060  relexpsucnnl  15065  relexpcnv  15070  relexpaddnn  15086  replim  15151  cjreb  15158  cjexp  15185  absexp  15339  abs1m  15370  recan  15371  cnsqrt00  15427  isercoll2  15701  iseraltlem2  15715  iseraltlem3  15716  sumeq2ii  15725  zsum  15750  fsum  15752  fsumf1o  15755  sumss  15756  fsumcvg2  15759  fsumadd  15772  isummulc2  15794  fsum2d  15803  fsummulc2  15816  fsumconst  15822  modfsummods  15825  modfsummod  15826  fsumparts  15838  fsumrelem  15839  fsumiun  15853  binom  15862  bcxmas  15867  incexclem  15868  isumshft  15871  isumnn0nn  15874  climcndslem1  15881  climcndslem2  15882  mertenslem2  15917  clim2prod  15920  prodfrec  15927  prodeq2ii  15943  zprod  15969  fprod  15973  fprodf1o  15978  fprodser  15981  fprodmul  15992  fproddiv  15993  prodsn  15994  prodsnf  15996  fprodabs  16006  fprodconst  16010  fprod2d  16013  fprodmodd  16029  binomfallfac  16073  bpolydif  16087  fprodefsum  16127  efne0  16129  efexp  16133  demoivreALT  16233  moddvds  16297  bitsinv1  16475  sadadd2  16493  smu01lem  16518  smupval  16521  smueqlem  16523  smumullem  16525  gcdaddm  16558  bezoutlem1  16572  bezout  16576  gcddiv  16584  seq1st  16604  alginv  16608  algfx  16613  lcmneg  16636  lcmid  16642  lcmgcdeq  16645  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem  16674  lcmfunsn  16677  lcmfun  16678  divgcdcoprm0  16698  cncongr1  16700  cncongr2  16701  nn0gcdsq  16785  crth  16811  eulerthlem2  16815  pythagtriplem1  16849  iserodd  16868  pcqmul  16886  pcexp  16892  pcneg  16907  pcmpt  16925  pcfac  16932  prmreclem2  16950  prmreclem3  16951  1arith  16960  vdwpc  17013  ramcl  17062  prmop1  17071  imasval  17557  ercpbllem  17594  iscat  17716  iscatd  17717  catideu  17719  iscatd2  17725  catlid  17727  catrid  17728  catass  17730  homfeq  17738  comfeq  17750  catpropd  17753  moni  17783  epii  17790  sectffval  17797  sectfval  17798  oppcsect  17825  sectmon  17829  isfunc  17914  funcid  17920  funcco  17921  funcpropd  17953  isfull  17963  fthsect  17978  fthmon  17980  natfval  18000  isnat  18001  nati  18009  fucsect  18028  natpropd  18032  setcmon  18140  setcepi  18141  setcsect  18142  fthestrcsetc  18205  embedsetcestrclem  18212  fthsetcestrc  18220  evlfcl  18278  uncfcurf  18295  yoniso  18341  joinval  18434  meetval  18448  islat  18490  latdisdlem  18553  latdisd  18554  isclat  18557  isdlat  18579  dlatmjdi  18580  isacs5lem  18602  acsdrscl  18603  acsficl  18604  isps  18625  mgmidmo  18685  mgmlrid  18692  lidrideqd  18694  lidrididd  18695  grpinvalem  18698  grpinva  18699  gsumvalx  18701  gsumval2  18711  ismgmhm  18721  mgmhmpropd  18723  mgmhmlin  18724  mgmhmeql  18741  issgrp  18745  isnsgrp  18748  sgrpass  18750  sgrp1  18754  issgrpd  18755  sgrppropd  18756  ismndd  18781  mndpropd  18784  imasmnd2  18799  xpsmnd0  18803  mnd1  18804  mnd1id  18805  ismhm  18810  mhmpropd  18817  mhmlin  18818  mhmimalem  18849  mhmeql  18851  gsumccat  18866  gsumwmhm  18870  frmdgsum  18887  symggrplem  18909  smndex1mndlem  18934  smndex1n0mnd  18937  sgrp2rid2  18951  sgrp2nmndlem4  18953  isgrp  18969  grppropd  18981  isgrpd2e  18985  dfgrp2  18992  isgrpid2  19006  grpidd2  19007  grpinvfval  19008  grpinvfvalALT  19009  grpinv11  19037  grpinvpropd  19045  grpidssd  19046  grpinvssd  19047  grpsubrcan  19051  dfgrp3lem  19068  grplactcnv  19073  imasgrp2  19085  mhmlem  19092  mulgnn0p1  19115  mulgaddcom  19128  mulginvcom  19129  mulgneg2  19138  mulgnnass  19139  mulgnn0ass  19140  mulgass  19141  mhmmulg  19145  cyccom  19233  isghm  19245  isghmOLD  19246  ghmlin  19251  ghmeql  19269  isga  19321  gagrpid  19324  gaass  19327  galcan  19334  orbsta  19343  cntzfval  19350  elcntz  19352  cntzsnval  19354  elcntzsn  19355  cntzi  19359  resscntz  19363  cntzmhm  19371  gsumwrev  19399  snsymgefmndeq  19426  cayleylem2  19445  symgextf1  19453  gsmsymgreqlem2  19463  gsmsymgreq  19464  symgfixf1  19469  pmtrfrn  19490  odfval  19564  odfvalALT  19565  mndodcong  19574  odbezout  19590  odeq1  19592  submod  19601  gexval  19610  gexdvds  19616  ispgp  19624  sylow1lem1  19630  sylow2alem1  19649  sylow2alem2  19650  sylow2blem2  19653  efgmnvl  19746  efgredlemc  19777  efgredeu  19784  frgpuptinv  19803  frgpup1  19807  frgpup3lem  19809  iscmn  19821  cmnpropd  19823  iscmnd  19826  abladdsub4  19843  submcmn2  19871  qusabl  19897  abl1  19898  imasabl  19908  iscyg  19911  cycsubmcmn  19921  gsum2dlem2  20003  telgsumfzs  20021  dmdprd  20032  dprdval  20037  dprdfcntz  20049  subgdmdprd  20068  dprd2da  20076  dpjrid  20096  pgpfac1lem3a  20110  ablfaclem3  20121  ablfac2  20123  isrng  20171  rngdi  20177  rngdir  20178  rngpropd  20191  imasrng  20194  ringurd  20202  issrg  20205  o2timesd  20227  rglcom4d  20228  srgmulgass  20234  srgpcomp  20235  srgbinom  20248  isring  20254  ringpropd  20301  ringinvnz1ne0  20313  mulgass2  20322  ring1  20323  imasring  20343  xpsring1d  20346  dvdsr  20378  dvreq1  20427  rnghmval  20456  isrnghm  20457  rnghmmul  20465  c0snmgmhm  20478  rngisomring1  20484  zrrnghm  20552  islring  20556  rngcsect  20652  ringcsect  20686  rrgval  20713  unitrrg  20719  domnlcanb  20736  domnrcanb  20738  isdrng  20749  drngprop  20760  isdrngd  20781  isdrngdOLD  20783  drngpropd  20785  cntzsdrg  20819  isabv  20828  abvmul  20838  issrng  20861  issrngd  20872  idsrngd  20873  islmod  20878  lmodlema  20879  islmodd  20880  lmodvsmmulgdi  20911  lmodprop2d  20938  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  islmhm  21043  lmhmlin  21051  islmhm2  21054  lmhmeql  21071  lmhmpropd  21089  islbs  21092  lbspropd  21115  rnglidlmsgrp  21273  rnglidlrng  21274  quscrng  21310  rngqiprngimfo  21328  islpir  21355  cnfldmulg  21433  cnfldexp  21434  prmirredlem  21500  pzriprnglem6  21514  pzriprnglem10  21518  pzriprnglem12  21520  chrcong  21559  zndvds  21585  znf1o  21587  znunit  21599  cygznlem3  21605  frgpcyg  21609  psgndiflemB  21635  isphl  21663  ipcj  21669  iporthcom  21670  ip2eq  21688  isphld  21689  phlpropd  21690  phlssphl  21694  ocvfval  21701  iscss  21718  ishil  21755  isobs  21757  obsip  21758  obslbs  21767  frlmphl  21818  isassa  21893  assalem  21894  isassad  21902  assapropd  21909  assamulgscm  21938  mvrf1  22023  mplmonmul  22071  mplcoe1  22072  mplcoe3  22073  mplcoe5lem  22074  mplcoe5  22075  evlslem1  22123  mpfrcl  22126  evlsval  22127  coe1tm  22291  ply1sclf1  22307  ply1coe  22317  eqcoe1ply1eq  22318  cply1coe0bi  22321  coe1fzgsumd  22323  ply1scleq  22324  ply1chr  22325  gsumply1eq  22328  evl1gsumd  22376  mat0dimcrng  22491  mat1ghm  22504  mat1mhm  22505  dmatcrng  22523  scmateALT  22533  scmatcrng  22542  scmatf1  22552  mvmumamul1  22575  mdetdiagid  22621  mdetralt  22629  mdetunilem1  22633  mdetunilem3  22635  mdetunilem4  22636  mdetunilem7  22639  mdetunilem9  22641  mdetuni0  22642  madugsum  22664  smadiadetr  22696  mat2pmatf1  22750  m2cpminvid2lem  22775  decpmataa0  22789  pmatcollpw2lem  22798  pm2mpf1  22820  chcoeffeqlem  22906  chcoeffeq  22907  cayhamlem3  22908  cayleyhamilton1  22913  isperf  23174  restperf  23207  cmpsub  23423  isconn  23436  2ndcsep  23482  elptr2  23597  ptbasin  23600  dfac14  23641  txcnp  23643  ptcnplem  23644  ptcnp  23645  cnmpt11  23686  cnmpt21  23694  cnmptcom  23701  kqfeq  23747  isr0  23760  pt1hmeo  23829  ustexsym  24239  isusp  24285  imasdsf1olem  24398  isxms  24472  xmspropd  24498  imasf1oxms  24517  stdbdmopn  24546  isngp3  24626  ngppropd  24665  tngngp3  24692  isnlm  24711  nmvs  24712  xrsxmet  24844  cnheibor  25000  htpyi  25019  htpycc  25025  pi1xfr  25101  pi1coghm  25107  isclm  25110  lmhmclm  25133  isclmp  25143  clmmulg  25147  iscph  25217  tcphcph  25284  cphsscph  25298  cmetcaulem  25335  bcth3  25378  ovolunlem1a  25544  ovolicc2lem1  25565  ovolicc2lem4  25568  ovolicc2  25570  mblsplit  25580  volun  25593  volfiniun  25595  voliunlem1  25598  volsup  25604  ioorinv  25624  uniioombllem2  25631  vitalilem3  25658  mbfeqalem1  25689  mbflim  25716  itgeqa  25863  itgconst  25868  itgfsum  25876  itgsplitioo  25887  dvnadd  25979  dvnres  25981  dvexp  26005  dvmptfsum  26027  mvth  26045  dvlip  26046  lhop1lem  26066  dvcvx  26073  mdegle0  26130  ply1nzb  26176  mon1pval  26195  facth1  26220  ig1pval  26229  dgrmulc  26325  dgrcolem1  26327  dgrcolem2  26328  dgrco  26329  coecj  26332  coecjOLD  26334  vieta1lem2  26367  vieta1  26368  elqaalem3  26377  dvntaylp  26427  ulmss  26454  mtest  26461  sineq0  26580  efif1olem4  26601  cxpexp  26724  mulcxplem  26740  mulcxp  26741  cxpmul2  26745  cxpeq  26814  affineequiv2  26881  quad2  26896  dcubic  26903  leibpi  26999  o1cxp  27032  scvxcvx  27043  facgam  27123  wilthlem1  27125  wilthlem2  27126  mpodvdsmulf1o  27251  fsumdvdsmul  27252  perfect  27289  dchrelbas2  27295  dchrinv  27319  dchrptlem2  27323  lgsne0  27393  lgsqrlem2  27405  lgsdchr  27413  gausslemma2d  27432  lgseisenlem2  27434  lgsquad2lem2  27443  2lgslem1a  27449  2lgslem1b  27450  dchrisumlem1  27547  qabvexp  27684  ostthlem1  27685  ostthlem2  27686  ostth3  27696  sltval2  27715  sltres  27721  nolesgn2ores  27731  nogesgn1ores  27733  nolt02o  27754  nogt01o  27755  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  noinfcbv  27776  noinfno  27777  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  addsrid  28011  addscom  28013  addscan1  28041  addsass  28052  mulsrid  28153  mulscom  28179  addsdilem3  28193  addsdilem4  28194  addsdi  28195  mulsasslem3  28205  mulsass  28206  mulscan2d  28219  mulscan1d  28220  om2noseqrdg  28324  n0scut  28352  cutpw2  28431  pw2cut  28434  elreno  28441  istrkgc  28476  istrkgcb  28478  istrkgld  28481  istrkg2ld  28482  axtgcgrrflx  28484  axtgupdim2  28493  tgjustf  28495  tgjustr  28496  iscgrg  28534  iscgrglt  28536  trgcgrg  28537  tgcgr4  28553  motcgr  28558  legso  28621  mirval  28677  israg  28719  ismidb  28800  isinagd  28861  f1otrgds  28891  ttgval  28897  ttgvalOLD  28898  ttgitvval  28910  brcgr  28929  brbtwn2  28934  colinearalglem1  28935  colinearalg  28939  ax5seglem1  28957  ax5seglem2  28958  ax5seglem8  28965  ax5seglem9  28966  axlowdimlem13  28983  axlowdimlem16  28986  axlowdim1  28988  axcontlem1  28993  axcontlem2  28994  axcontlem6  28998  axcontlem7  28999  axcontlem8  29000  ecgrtg  29012  usgredg2v  29258  issubgr  29302  cplgruvtxb  29444  cusgrsize  29486  finsumvtxdg2size  29582  isrgr  29591  wkslem1  29639  wkslem2  29640  iswlk  29642  uspgr2wlkeq  29678  2wlklem  29699  wlkres  29702  redwlk  29704  wlkp1lem6  29710  wlkp1lem7  29711  wlkp1lem8  29712  pthdivtx  29761  upgrwlkdvdelem  29768  isclwlk  29805  iscrct  29822  iscycl  29823  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  wwlksnextinj  29928  rusgrnumwwlk  30004  clwlkclwwlklem2  30028  clwlkclwwlkf1lem3  30034  clwlkclwwlkf1  30038  erclwwlkeq  30046  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  erclwwlkneq  30095  clwwlkvbij  30141  upgreupthseg  30237  eupth2eucrct  30245  eupth2lem3  30264  eupth2  30267  eucrctshift  30271  2clwwlk  30375  numclwwlk1lem2f1  30385  numclwlk1lem1  30397  numclwlk1lem2  30398  numclwlk2lem2f1o  30407  isgrpo  30525  grpoass  30531  grpoidinvlem3  30534  grpoidinv  30536  grpoideu  30537  grpoidinv2  30543  grpoinvfval  30550  isablo  30574  ablocom  30576  vciOLD  30589  vcidOLD  30592  vcdi  30593  vcdir  30594  vcass  30595  isvclem  30605  isnvlem  30638  nvmeq0  30686  nvs  30691  imsmetlem  30718  islno  30781  lnolin  30782  ishmo  30839  isphg  30845  phpar2  30851  phpar  30852  ipdiri  30858  ipasslem1  30859  ipasslem5  30863  ipasslem11  30868  ipassi  30869  dipdir  30870  dipass  30873  ip2eqi  30884  htth  30946  hvsubsub4  31088  hvnegdi  31095  hvaddcan  31098  hvaddcan2  31099  hvsubcan  31102  hvsubcan2  31103  hvaddsub4  31106  hial2eq  31134  normlem9at  31149  normsq  31162  norm-iii  31168  normsub  31171  normpyth  31173  normpar  31183  polid  31187  issubgoilem  31288  ococ  31434  chj0  31525  chlejb1  31540  chdmm1  31553  chjass  31561  spanun  31573  spansn  31587  elspansn2  31595  cmbr  31612  cmbr3  31636  pjoml2  31639  pjoml3  31640  osum  31673  spansnj  31675  pjch1  31698  pjadji  31713  pjaddi  31714  pjinormi  31715  pjsubi  31716  pjmuli  31717  pjcjt2  31720  pjch  31722  pjopyth  31748  pjpyth  31753  hoaddcom  31802  hoaddass  31810  hocsubdir  31813  hoaddrid  31819  ho0sub  31825  honegsub  31827  adjsym  31861  eigrei  31862  eigre  31863  eigposi  31864  eigorth  31866  ellnop  31886  elhmop  31901  ellnfn  31911  cnvadj  31920  lnopl  31942  unop  31943  hmop  31950  lnfnl  31959  adj1  31961  eleigvec  31985  hoddi  32018  lnopeq0lem2  32034  lnopunilem1  32038  lnopunilem2  32039  lnopunii  32040  elunop2  32041  lnophmi  32046  lnfnmul  32076  cnlnadjlem5  32099  branmfn  32133  bra11  32136  hmopidmchi  32179  hmopidmch  32181  hmopidmpj  32182  pjss2coi  32192  pjssmi  32193  pjssge0i  32194  pjidmco  32209  dfpjop  32210  elpjrn  32218  isst  32241  ishst  32242  hstel2  32247  stj  32263  mdbr  32322  mdi  32323  mdbr3  32325  dmdbr  32327  dmdmd  32328  dmdi  32330  dmdbr3  32333  mddmd2  32337  mdsl1i  32349  chjatom  32385  iuninc  32580  fmptcof2  32673  bcm1n  32802  fsumiunle  32835  xmulcand  32887  xrsmulgzz  32993  gsumle  33083  psgnfzto1st  33107  isslmd  33190  slmdlema  33191  gsumvsca1  33214  gsumvsca2  33215  urpropd  33221  erlval  33244  domnlcanOLD  33263  qusvscpbl  33358  nsgqusf1olem3  33422  opprqusdrng  33500  ressply1mon1p  33572  ressply1invg  33573  ply1moneq  33590  fedgmul  33658  brfldext  33674  minplyval  33712  submateq  33769  dispcmp  33819  pstmxmet  33857  cnre2csqlem  33870  mndpluscn  33886  qqhval2  33944  isrrext  33962  esumfzf  34049  esumcvg  34066  esum2dlem  34072  esumiun  34074  ofcfeqd2  34081  ismeas  34179  isrnmeas  34180  measvun  34189  carsgval  34284  inelcarsg  34292  carsgclctunlem1  34298  carsgclctunlem2  34300  pmeasmono  34305  pmeasadd  34306  eulerpartlemgvv  34357  eulerpartlemn  34362  sseqp1  34376  probun  34400  sgnsgn  34529  breprexp  34626  istrkg2d  34659  axtgupdim2ALTV  34661  afsval  34664  bnj1385  34824  bnj66  34852  bnj106  34860  bnj155  34871  bnj222  34875  bnj540  34884  bnj591  34903  bnj594  34904  bnj611  34910  bnj893  34920  bnj1000  34933  bnj966  34936  bnj1112  34975  bnj1234  35005  bnj1253  35009  bnj1280  35012  bnj1326  35018  bnj1450  35042  bnj1463  35047  bnj1529  35062  f1resveqaeq  35077  pfxwlk  35107  revwlk  35108  subfacp1lem3  35166  subfacp1lem4  35167  subfacp1lem5  35168  subfacp1lem6  35169  subfacval2  35171  erdszelem9  35183  sconnpht  35213  ptpconn  35217  cvmliftmolem1  35265  cvmliftmolem2  35266  cvmliftlem10  35278  cvmlift2  35300  cvmliftphtlem  35301  satfdm  35353  gonarlem  35378  gonar  35379  goalr  35381  satfdmfmla  35384  prv  35412  mrsubff1  35498  mrsubccat  35502  elmrsubrn  35504  mrsubvrs  35506  elmpst  35520  msrid  35529  msubvrs  35544  sqdivzi  35707  shftvalg  35711  bcprod  35717  bccolsum  35718  iprodefisumlem  35719  faclimlem1  35722  rdgprc  35775  dfrdg2  35776  elwlim  35804  fvsingle  35901  fullfunfv  35928  lineelsb2  36129  rankung  36147  ranksng  36148  rankpwg  36150  opnregcld  36312  cldregopn  36313  neibastop3  36344  weiunlem1  36444  bj-sbeqALT  36882  bj-gabeqis  36920  bj-isclm  37273  rdgeqoa  37352  fvineqsnf1  37392  tan2h  37598  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem9  37615  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem19  37625  broucube  37640  voliunnfl  37650  volsupnfl  37651  cocanfo  37705  upixp  37715  sdclem2  37728  caushft  37747  ismtycnv  37788  ismtyima  37789  ismtybndlem  37792  ismtyres  37794  bfplem2  37809  bfp  37810  isass  37832  opidonOLD  37838  exidu1  37842  cmpidelt  37845  grpoeqdivid  37867  elghomlem2OLD  37872  ghomlinOLD  37874  ghomco  37877  isrngo  37883  rngoid  37888  rngoideu  37889  rngodi  37890  rngodir  37891  rngoass  37892  rngohomval  37950  isrngohom  37951  rngohomadd  37955  rngohommul  37956  iscom2  37981  iscringd  37984  crngocom  37987  crngohomfo  37992  dmncan2  38063  elsymrels4  38536  brredunds  38607  lshpset  38959  lcvexchlem4  39018  lcvexchlem5  39019  lflset  39040  islfl  39041  lfli  39042  islfld  39043  eqlkr3  39082  isopos  39161  oposlem  39163  opcon3b  39177  cmtvalN  39192  omllaw  39224  cvlexchb2  39312  cvlatexchb2  39316  cvlsupr2  39324  4atlem9  39585  4atlem10a  39586  4atlem11a  39589  4atlem12a  39592  4at2  39596  pmapglb2N  39753  pmapglb2xN  39754  paddasslem17  39818  ispsubclN  39919  ispsubcl2N  39929  lhpmod2i2  40020  lhpmod6i1  40021  4atexlemex2  40053  4atex  40058  4atex2-0aOLDN  40060  4atex2-0cOLDN  40062  ldilval  40095  ltrnfset  40099  ltrnset  40100  isltrn  40101  ltrneq2  40130  trnfsetN  40137  trnsetN  40138  istrnN  40139  cdlemd5  40184  cdleme0moN  40207  cdleme0nex  40272  cdleme18d  40277  cdleme31so  40361  cdleme31fv  40372  cdlemg2jlemOLDN  40575  cdlemg2fvlem  40576  cdlemg2klem  40577  istendo  40742  tendovalco  40747  tendoeq2  40756  dicelvalN  41160  dihval  41214  dihcnv11  41257  dihmeetlem13N  41301  dihlspsnat  41315  dochn0nv  41357  dochkrshp4  41371  lpolsetN  41464  lpolsatN  41470  lpolpolsatN  41471  lcfl1lem  41473  lclkrlem2a  41489  lclkrlem2e  41493  lcfls1lem  41516  lclkrs2  41522  lcdfval  41570  lcdval  41571  mapdffval  41608  mapdfval  41609  mapd0  41647  mapdpglem30  41684  mapdhval  41706  mapdheq2  41711  hdmap1vallem  41779  hdmap1val  41780  hdmap1cbv  41784  hdmapval3N  41820  hdmap10  41822  hdmapeq0  41826  hdmap14lem12  41861  hdmap14lem13  41862  hgmapfval  41868  hgmapvs  41873  hgmapvv  41908  hlhilocv  41943  recbothd  41973  lcmineqlem13  42022  isprimroot  42074  primrootsunit1  42078  aks6d1c1p1  42088  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  evl1gprodd  42098  aks6d1c1rh  42106  aks6d1c2lem3  42107  deg1gprod  42121  deg1pow  42122  sticksstones22  42149  aks6d1c6lem2  42152  aks5lem3a  42170  unitscyglem2  42177  unitscyglem3  42178  unitscyglem4  42179  ccatcan2d  42270  remulcan2d  42276  nnadd1com  42280  nnaddcom  42281  nnadddir  42283  nnmul1com  42284  nnmulcom  42285  sumcubes  42325  expeqidd  42338  efne0d  42351  cxp112d  42355  cxp111d  42356  log11d  42360  sn-addcand  42425  sn-addcan2d  42427  sn-mullid  42441  nn0addcom  42456  renegmulnnass  42459  nn0mulcom  42460  zmulcomlem  42461  cnreeu  42476  abvexp  42518  fiabv  42522  prjsprel  42590  prjcrvfval  42617  flt0  42623  sn-isghm  42659  ismrcd2  42686  ismrc  42688  dvdsrabdioph  42797  fphpdo  42804  rmxypairf1o  42899  monotoddzzfi  42930  monotoddzz  42931  oddcomabszz  42932  rmxdioph  43004  expdiophlem2  43010  dnnumch3  43035  aomclem8  43049  islssfg  43058  unxpwdom3  43083  gicabl  43087  idomodle  43179  fgraphxp  43192  hausgraph  43193  onov0suclim  43263  oaabsb  43283  oaomoencom  43306  oenass  43308  omabs2  43321  tfsconcat0b  43335  nadd1suc  43381  naddonnn  43384  minregex  43523  relexpmulnn  43698  clsk1independent  44035  ntrclsk13  44060  ntrclsk4  44061  imo72b2  44161  grumnud  44281  nzss  44312  caofcan  44318  expgrowth  44330  fsneq  45148  fperiodmullem  45253  uzinico3  45515  fsumf1of  45529  fmuldfeq  45538  fprodexp  45549  fprodabs2  45550  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climaddf  45570  mullimc  45571  limcperiod  45583  neglimc  45602  addlimc  45603  0ellimcdiv  45604  climeldmeqmpt  45623  climfveqmpt  45626  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  climeqf  45643  climeldmeqmpt3  45644  limsupequz  45678  cncfperiod  45834  icccncfext  45842  fperdvper  45874  dvnmptdivc  45893  dvnxpaek  45897  dvnmul  45898  dvmptfprod  45900  dvnprodlem3  45903  itgspltprt  45934  stoweidlem30  45985  stoweidlem48  46003  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  fourierdlem50  46111  fourierdlem73  46134  fourierdlem81  46142  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem94  46155  fourierdlem97  46158  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  sge0iunmptlemfi  46368  ismea  46406  meadjuni  46412  meaiuninclem  46435  caragenval  46448  isome  46449  caragensplit  46455  carageniuncllem1  46476  caratheodorylem1  46481  hoidmvlelem3  46552  vonvolmbllem  46615  vonvolmbl  46616  smflimlem3  46728  smflim  46732  smfpimcc  46763  smfsuplem2  46767  fsetsnf1  47001  cfsetsnfsetf1  47008  fcoresf1  47018  csbafv12g  47086  csbaovg  47129  csbafv212g  47168  fargshiftf1  47365  fargshiftfva  47367  prproropf1olem4  47430  fmtnorec2  47467  fmtnoprmfac1lem  47488  fmtnofac1  47494  quad1  47544  requad1  47546  perfectALTV  47647  fpprwppr  47663  nfermltl8rev  47666  nfermltl2rev  47667  nfermltlrev  47668  sbgoldbo  47711  isgrim  47805  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  grimco  47817  gricushgr  47823  isubgrgrim  47834  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  uspgrlimlem3  47892  uspgrlimlem4  47893  grlimgrtrilem2  47897  gpgvtxedg0  47955  gpgvtxedg1  47956  uspgrsprf1  47990  plusfreseq  48007  iscomlaw  48033  isasslaw  48035  lidldomn1  48074  zlidlring  48077  rngcsectALTV  48118  ringcsectALTV  48152  ovmpordxf  48183  lmodvsmdi  48223  islininds  48291  lindslinindimp2lem4  48306  lindslinindsimp2  48308  lmod1  48337  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdig  48472  1arymaptf1  48491  2arymaptf1  48502  itcovalpc  48521  itcovalt2  48526  rrx2pnecoorneor  48564  rrx2plordisom  48572  rrx2line  48589  rrx2linest  48591  line2ylem  48600  line2x  48603  line2y  48604  itscnhlc0yqe  48608  itscnhlc0xyqsol  48614  idmon  48804  idepi  48805  grptcmon  48901  grptcepi  48902  aacllem  49031