Theorem eqeq12d 2753

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 2751	. 2 ⊢ ((𝜑 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	anidms 566	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  neeq12d  3002  cdeqeq  3781  sbceqg  4412  csbun  4441  csbin  4442  csbdif  4524  csbif  4583  iununi  5099  csbopab  5560  csbopabgALT  5561  dfid2  5580  csbima12  6097  dmsnsnsn  6240  csbcog  6317  dfpred3g  6333  preddowncl  6353  limeq  6396  csbiota  6554  fveqres  6953  opabiota  6991  fvmptf  7037  eqfnfv2f  7055  fvreseq0  7058  fveqdmss  7098  fvcofneq  7113  fnressn  7178  fnelfp  7195  fprb  7214  fnprb  7228  fntpb  7229  f1cofveqaeqALT  7279  nvocnv  7301  cocan1  7311  cocan2  7312  2fvcoidd  7317  fliftfun  7332  weniso  7374  csbriota  7403  oveqrspc2v  7458  csbov123  7475  eqfnov  7562  ovmpos  7581  ov2gf  7582  ovmpodxf  7583  caovcomg  7628  caovassg  7631  caovcang  7634  caovcanrd  7636  caovcan  7637  caovdig  7647  caovdirg  7650  caovmo  7670  coof  7721  offveqb  7724  caofid0l  7730  caofid0r  7731  caofidlcan  7735  caofass  7737  caonncan  7741  ordunisuc  7852  onsucuni2  7854  orduninsuc  7864  op1stg  8026  op2ndg  8027  f1o2ndf1  8147  xpord2pred  8170  xpord3pred  8177  poseq  8183  soseq  8184  fnsuppres  8216  csbfrecsg  8309  fpr3g  8310  frrlem1  8311  frrlem12  8322  frrlem13  8323  fpr2a  8327  wfr3g  8347  wfrlem1OLD  8348  wfrlem3OLDa  8351  wfrlem12OLD  8360  wfrlem14OLD  8362  wfrlem15OLD  8363  wfr2aOLD  8366  onfununi  8381  tfrlem1  8416  tfrlem3a  8417  tfrlem5  8420  tfrlem9  8425  tfrlem11  8428  tfrlem12  8429  tfr3  8439  tz7.44-1  8446  tz7.44-2  8447  tz7.44-3  8448  rdglem1  8455  rdg0g  8467  seqomlem1  8490  oalim  8570  omlim  8571  oelim  8572  oa0r  8576  om0r  8577  om1r  8581  oaass  8599  oarec  8600  odi  8617  omass  8618  oelim2  8633  oeoalem  8634  oeoa  8635  oeoelem  8636  oeoe  8637  nna0r  8647  nnacom  8655  nnaass  8660  nndi  8661  nnmass  8662  nnmsucr  8663  nnmcom  8664  oaabs  8686  oaabs2  8687  omabs  8689  naddcllem  8714  naddcom  8720  naddrid  8721  naddass  8734  naddsuc2  8739  naddoa  8740  ecovcom  8863  ecovass  8864  ecovdi  8865  dom2lem  9032  unxpdomlem2  9287  unxpdomlem3  9288  ixpfi2  9390  fipreima  9398  ordiso2  9555  wemaplem1  9586  wemaplem2  9587  wemapsolem  9590  cantnfval2  9709  cantnfp1lem3  9720  oemapvali  9724  cantnflem1c  9727  cantnflem1  9729  wemapwe  9737  rnttrcl  9762  tcvalg  9778  frr3g  9796  frr2  9800  rankvalg  9857  rankonidlem  9868  ranklim  9884  rankuni  9903  updjud  9974  cardprclem  10019  cardprc  10020  carduni  10021  fseqenlem1  10064  fodomacn  10096  alephcard  10110  alephfp2  10149  alephval3  10150  dfac12lem1  10184  dfac12lem2  10185  dfac12r  10187  ackbij1lem8  10266  ackbij1lem14  10272  ackbij1lem16  10274  ackbij2lem3  10280  cardcf  10292  sornom  10317  fin23lem28  10380  isf32lem2  10394  itunitc  10461  ituniiun  10462  axdc3lem2  10491  axdc4lem  10495  ttukeylem3  10551  ttukey2g  10556  fpwwe2lem7  10677  fpwwecbv  10684  canth4  10687  pwfseqlem2  10699  addcanpi  10939  mulcanpi  10940  recrecnq  11007  ltexnq  11015  genpv  11039  0idsr  11137  1idsr  11138  ax1rid  11201  mulrid  11259  addcan  11445  addcan2  11446  mulcand  11896  mulcan2d  11897  mulcan2g  11917  div11OLD  11951  divmuleq  11972  conjmul  11984  eqneg  11987  ofsubeq0  12263  rpnnen1lem6  13024  cnref1o  13027  xmulasslem  13327  xmulass  13329  xadddi2  13339  prunioo  13521  fzsuc2  13622  fzprval  13625  fztpval  13626  fzosplitprm1  13816  modadd1  13948  modmul1  13965  addmodlteq  13987  om2uzsuci  13989  om2uzrdg  13997  uzrdgxfr  14008  seq1  14055  seqp1  14057  seqfveq2  14065  seqfveq  14067  seqshft2  14069  seqsplit  14076  seqcaopr3  14078  seqcaopr2  14079  seqf1olem2a  14081  seqf1olem2  14083  seqf1o  14084  seqid  14088  seqid2  14089  seqhomo  14090  ser1const  14099  seqof2  14101  mulexp  14142  expadd  14145  expmul  14148  binom2  14256  sq01  14264  modexp  14277  bcpasc  14360  hashgadd  14416  hashdom  14418  hashfzo  14468  hashfzp1  14470  hashxplem  14472  hashxp  14473  hashmap  14474  hashpw  14475  hashbclem  14491  hashbc  14492  hashfacen  14493  hashf1lem1  14494  hashf1lem2  14495  hashf1  14496  seqcoll  14503  eqs1  14650  swrdspsleq  14703  pfxeq  14734  pfxsuff1eqwrdeq  14737  ccatopth2  14755  cats1un  14759  swrdccatin1  14763  swrdccat3blem  14777  cshf1  14848  repswcshw  14850  s2eq2s1eq  14975  s3eqs2s1eq  14977  pfx2  14986  2swrd2eqwrdeq  14992  wwlktovf1  14996  eqwrds3  15000  relexpsucnnr  15064  relexpsucnnl  15069  relexpcnv  15074  relexpaddnn  15090  replim  15155  cjreb  15162  cjexp  15189  absexp  15343  abs1m  15374  recan  15375  cnsqrt00  15431  isercoll2  15705  iseraltlem2  15719  iseraltlem3  15720  sumeq2ii  15729  zsum  15754  fsum  15756  fsumf1o  15759  sumss  15760  fsumcvg2  15763  fsumadd  15776  isummulc2  15798  fsum2d  15807  fsummulc2  15820  fsumconst  15826  modfsummods  15829  modfsummod  15830  fsumparts  15842  fsumrelem  15843  fsumiun  15857  binom  15866  bcxmas  15871  incexclem  15872  isumshft  15875  isumnn0nn  15878  climcndslem1  15885  climcndslem2  15886  mertenslem2  15921  clim2prod  15924  prodfrec  15931  prodeq2ii  15947  zprod  15973  fprod  15977  fprodf1o  15982  fprodser  15985  fprodmul  15996  fproddiv  15997  prodsn  15998  prodsnf  16000  fprodabs  16010  fprodconst  16014  fprod2d  16017  fprodmodd  16033  binomfallfac  16077  bpolydif  16091  fprodefsum  16131  efne0  16133  efexp  16137  demoivreALT  16237  moddvds  16301  bitsinv1  16479  sadadd2  16497  smu01lem  16522  smupval  16525  smueqlem  16527  smumullem  16529  gcdaddm  16562  bezoutlem1  16576  bezout  16580  gcddiv  16588  seq1st  16608  alginv  16612  algfx  16617  lcmneg  16640  lcmid  16646  lcmgcdeq  16649  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem  16678  lcmfunsn  16681  lcmfun  16682  divgcdcoprm0  16702  cncongr1  16704  cncongr2  16705  nn0gcdsq  16789  crth  16815  eulerthlem2  16819  pythagtriplem1  16854  iserodd  16873  pcqmul  16891  pcexp  16897  pcneg  16912  pcmpt  16930  pcfac  16937  prmreclem2  16955  prmreclem3  16956  1arith  16965  vdwpc  17018  ramcl  17067  prmop1  17076  imasval  17556  ercpbllem  17593  iscat  17715  iscatd  17716  catideu  17718  iscatd2  17724  catlid  17726  catrid  17727  catass  17729  homfeq  17737  comfeq  17749  catpropd  17752  moni  17780  epii  17787  sectffval  17794  sectfval  17795  oppcsect  17822  sectmon  17826  isfunc  17909  funcid  17915  funcco  17916  funcpropd  17947  isfull  17957  fthsect  17972  fthmon  17974  natfval  17994  isnat  17995  nati  18003  fucsect  18020  natpropd  18024  setcmon  18132  setcepi  18133  setcsect  18134  fthestrcsetc  18195  embedsetcestrclem  18202  fthsetcestrc  18210  evlfcl  18267  uncfcurf  18284  yoniso  18330  joinval  18422  meetval  18436  islat  18478  latdisdlem  18541  latdisd  18542  isclat  18545  isdlat  18567  dlatmjdi  18568  isacs5lem  18590  acsdrscl  18591  acsficl  18592  isps  18613  mgmidmo  18673  mgmlrid  18680  lidrideqd  18682  lidrididd  18683  grpinvalem  18686  grpinva  18687  gsumvalx  18689  gsumval2  18699  ismgmhm  18709  mgmhmpropd  18711  mgmhmlin  18712  mgmhmeql  18729  issgrp  18733  isnsgrp  18736  sgrpass  18738  sgrp1  18742  issgrpd  18743  sgrppropd  18744  ismndd  18769  mndpropd  18772  imasmnd2  18787  xpsmnd0  18791  mnd1  18792  mnd1id  18793  ismhm  18798  mhmpropd  18805  mhmlin  18806  mhmimalem  18837  mhmeql  18839  gsumccat  18854  gsumwmhm  18858  frmdgsum  18875  symggrplem  18897  smndex1mndlem  18922  smndex1n0mnd  18925  sgrp2rid2  18939  sgrp2nmndlem4  18941  isgrp  18957  grppropd  18969  isgrpd2e  18973  dfgrp2  18980  isgrpid2  18994  grpidd2  18995  grpinvfval  18996  grpinvfvalALT  18997  grpinv11  19025  grpinvpropd  19033  grpidssd  19034  grpinvssd  19035  grpsubrcan  19039  dfgrp3lem  19056  grplactcnv  19061  imasgrp2  19073  mhmlem  19080  mulgnn0p1  19103  mulgaddcom  19116  mulginvcom  19117  mulgneg2  19126  mulgnnass  19127  mulgnn0ass  19128  mulgass  19129  mhmmulg  19133  cyccom  19221  isghm  19233  isghmOLD  19234  ghmlin  19239  ghmeql  19257  isga  19309  gagrpid  19312  gaass  19315  galcan  19322  orbsta  19331  cntzfval  19338  elcntz  19340  cntzsnval  19342  elcntzsn  19343  cntzi  19347  resscntz  19351  cntzmhm  19359  gsumwrev  19385  snsymgefmndeq  19412  cayleylem2  19431  symgextf1  19439  gsmsymgreqlem2  19449  gsmsymgreq  19450  symgfixf1  19455  pmtrfrn  19476  odfval  19550  odfvalALT  19551  mndodcong  19560  odbezout  19576  odeq1  19578  submod  19587  gexval  19596  gexdvds  19602  ispgp  19610  sylow1lem1  19616  sylow2alem1  19635  sylow2alem2  19636  sylow2blem2  19639  efgmnvl  19732  efgredlemc  19763  efgredeu  19770  frgpuptinv  19789  frgpup1  19793  frgpup3lem  19795  iscmn  19807  cmnpropd  19809  iscmnd  19812  abladdsub4  19829  submcmn2  19857  qusabl  19883  abl1  19884  imasabl  19894  iscyg  19897  cycsubmcmn  19907  gsum2dlem2  19989  telgsumfzs  20007  dmdprd  20018  dprdval  20023  dprdfcntz  20035  subgdmdprd  20054  dprd2da  20062  dpjrid  20082  pgpfac1lem3a  20096  ablfaclem3  20107  ablfac2  20109  isrng  20151  rngdi  20157  rngdir  20158  rngpropd  20171  imasrng  20174  ringurd  20182  issrg  20185  o2timesd  20207  rglcom4d  20208  srgmulgass  20214  srgpcomp  20215  srgbinom  20228  isring  20234  ringpropd  20285  ringinvnz1ne0  20297  mulgass2  20306  ring1  20307  imasring  20327  xpsring1d  20330  dvdsr  20362  dvreq1  20411  rnghmval  20440  isrnghm  20441  rnghmmul  20449  c0snmgmhm  20462  rngisomring1  20468  zrrnghm  20536  islring  20540  rngcsect  20636  ringcsect  20670  rrgval  20697  unitrrg  20703  domnlcanb  20720  domnrcanb  20722  isdrng  20733  drngprop  20744  isdrngd  20765  isdrngdOLD  20767  drngpropd  20769  cntzsdrg  20803  isabv  20812  abvmul  20822  issrng  20845  issrngd  20856  idsrngd  20857  islmod  20862  lmodlema  20863  islmodd  20864  lmodvsmmulgdi  20895  lmodprop2d  20922  rmodislmodlem  20927  rmodislmod  20928  islmhm  21026  lmhmlin  21034  islmhm2  21037  lmhmeql  21054  lmhmpropd  21072  islbs  21075  lbspropd  21098  rnglidlmsgrp  21256  rnglidlrng  21257  quscrng  21293  rngqiprngimfo  21311  islpir  21338  cnfldmulg  21416  cnfldexp  21417  prmirredlem  21483  pzriprnglem6  21497  pzriprnglem10  21501  pzriprnglem12  21503  chrcong  21542  zndvds  21568  znf1o  21570  znunit  21582  cygznlem3  21588  frgpcyg  21592  psgndiflemB  21618  isphl  21646  ipcj  21652  iporthcom  21653  ip2eq  21671  isphld  21672  phlpropd  21673  phlssphl  21677  ocvfval  21684  iscss  21701  ishil  21738  isobs  21740  obsip  21741  obslbs  21750  frlmphl  21801  isassa  21876  assalem  21877  isassad  21885  assapropd  21892  assamulgscm  21921  mvrf1  22006  mplmonmul  22054  mplcoe1  22055  mplcoe3  22056  mplcoe5lem  22057  mplcoe5  22058  evlslem1  22106  mpfrcl  22109  evlsval  22110  psdpw  22174  coe1tm  22276  ply1sclf1  22292  ply1coe  22302  eqcoe1ply1eq  22303  cply1coe0bi  22306  coe1fzgsumd  22308  ply1scleq  22309  ply1chr  22310  gsumply1eq  22313  evl1gsumd  22361  mat0dimcrng  22476  mat1ghm  22489  mat1mhm  22490  dmatcrng  22508  scmateALT  22518  scmatcrng  22527  scmatf1  22537  mvmumamul1  22560  mdetdiagid  22606  mdetralt  22614  mdetunilem1  22618  mdetunilem3  22620  mdetunilem4  22621  mdetunilem7  22624  mdetunilem9  22626  mdetuni0  22627  madugsum  22649  smadiadetr  22681  mat2pmatf1  22735  m2cpminvid2lem  22760  decpmataa0  22774  pmatcollpw2lem  22783  pm2mpf1  22805  chcoeffeqlem  22891  chcoeffeq  22892  cayhamlem3  22893  cayleyhamilton1  22898  isperf  23159  restperf  23192  cmpsub  23408  isconn  23421  2ndcsep  23467  elptr2  23582  ptbasin  23585  dfac14  23626  txcnp  23628  ptcnplem  23629  ptcnp  23630  cnmpt11  23671  cnmpt21  23679  cnmptcom  23686  kqfeq  23732  isr0  23745  pt1hmeo  23814  ustexsym  24224  isusp  24270  imasdsf1olem  24383  isxms  24457  xmspropd  24483  imasf1oxms  24502  stdbdmopn  24531  isngp3  24611  ngppropd  24650  tngngp3  24677  isnlm  24696  nmvs  24697  xrsxmet  24831  cnheibor  24987  htpyi  25006  htpycc  25012  pi1xfr  25088  pi1coghm  25094  isclm  25097  lmhmclm  25120  isclmp  25130  clmmulg  25134  iscph  25204  tcphcph  25271  cphsscph  25285  cmetcaulem  25322  bcth3  25365  ovolunlem1a  25531  ovolicc2lem1  25552  ovolicc2lem4  25555  ovolicc2  25557  mblsplit  25567  volun  25580  volfiniun  25582  voliunlem1  25585  volsup  25591  ioorinv  25611  uniioombllem2  25618  vitalilem3  25645  mbfeqalem1  25676  mbflim  25703  itgeqa  25849  itgconst  25854  itgfsum  25862  itgsplitioo  25873  dvnadd  25965  dvnres  25967  dvexp  25991  dvmptfsum  26013  mvth  26031  dvlip  26032  lhop1lem  26052  dvcvx  26059  mdegle0  26116  ply1nzb  26162  mon1pval  26181  facth1  26206  ig1pval  26215  dgrmulc  26311  dgrcolem1  26313  dgrcolem2  26314  dgrco  26315  coecj  26318  coecjOLD  26320  vieta1lem2  26353  vieta1  26354  elqaalem3  26363  dvntaylp  26413  ulmss  26440  mtest  26447  sineq0  26566  efif1olem4  26587  cxpexp  26710  mulcxplem  26726  mulcxp  26727  cxpmul2  26731  cxpeq  26800  affineequiv2  26867  quad2  26882  dcubic  26889  leibpi  26985  o1cxp  27018  scvxcvx  27029  facgam  27109  wilthlem1  27111  wilthlem2  27112  mpodvdsmulf1o  27237  fsumdvdsmul  27238  perfect  27275  dchrelbas2  27281  dchrinv  27305  dchrptlem2  27309  lgsne0  27379  lgsqrlem2  27391  lgsdchr  27399  gausslemma2d  27418  lgseisenlem2  27420  lgsquad2lem2  27429  2lgslem1a  27435  2lgslem1b  27436  dchrisumlem1  27533  qabvexp  27670  ostthlem1  27671  ostthlem2  27672  ostth3  27682  sltval2  27701  sltres  27707  nolesgn2ores  27717  nogesgn1ores  27719  nolt02o  27740  nogt01o  27741  nosupcbv  27747  nosupno  27748  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  noinfcbv  27762  noinfno  27763  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem3  27770  noinfbnd1lem5  27772  addsrid  27997  addscom  27999  addscan1  28027  addsass  28038  mulsrid  28139  mulscom  28165  addsdilem3  28179  addsdilem4  28180  addsdi  28181  mulsasslem3  28191  mulsass  28192  mulscan2d  28205  mulscan1d  28206  om2noseqrdg  28310  n0scut  28338  cutpw2  28417  pw2cut  28420  elreno  28427  istrkgc  28462  istrkgcb  28464  istrkgld  28467  istrkg2ld  28468  axtgcgrrflx  28470  axtgupdim2  28479  tgjustf  28481  tgjustr  28482  iscgrg  28520  iscgrglt  28522  trgcgrg  28523  tgcgr4  28539  motcgr  28544  legso  28607  mirval  28663  israg  28705  ismidb  28786  isinagd  28847  f1otrgds  28877  ttgval  28883  ttgvalOLD  28884  ttgitvval  28896  brcgr  28915  brbtwn2  28920  colinearalglem1  28921  colinearalg  28925  ax5seglem1  28943  ax5seglem2  28944  ax5seglem8  28951  ax5seglem9  28952  axlowdimlem13  28969  axlowdimlem16  28972  axlowdim1  28974  axcontlem1  28979  axcontlem2  28980  axcontlem6  28984  axcontlem7  28985  axcontlem8  28986  ecgrtg  28998  usgredg2v  29244  issubgr  29288  cplgruvtxb  29430  cusgrsize  29472  finsumvtxdg2size  29568  isrgr  29577  wkslem1  29625  wkslem2  29626  iswlk  29628  uspgr2wlkeq  29664  2wlklem  29685  wlkres  29688  redwlk  29690  wlkp1lem6  29696  wlkp1lem7  29697  wlkp1lem8  29698  pthdivtx  29747  upgrwlkdvdelem  29756  isclwlk  29793  iscrct  29810  iscycl  29811  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  wwlksnextinj  29919  rusgrnumwwlk  29995  clwlkclwwlklem2  30019  clwlkclwwlkf1lem3  30025  clwlkclwwlkf1  30029  erclwwlkeq  30037  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  erclwwlkneq  30086  clwwlkvbij  30132  upgreupthseg  30228  eupth2eucrct  30236  eupth2lem3  30255  eupth2  30258  eucrctshift  30262  2clwwlk  30366  numclwwlk1lem2f1  30376  numclwlk1lem1  30388  numclwlk1lem2  30389  numclwlk2lem2f1o  30398  isgrpo  30516  grpoass  30522  grpoidinvlem3  30525  grpoidinv  30527  grpoideu  30528  grpoidinv2  30534  grpoinvfval  30541  isablo  30565  ablocom  30567  vciOLD  30580  vcidOLD  30583  vcdi  30584  vcdir  30585  vcass  30586  isvclem  30596  isnvlem  30629  nvmeq0  30677  nvs  30682  imsmetlem  30709  islno  30772  lnolin  30773  ishmo  30830  isphg  30836  phpar2  30842  phpar  30843  ipdiri  30849  ipasslem1  30850  ipasslem5  30854  ipasslem11  30859  ipassi  30860  dipdir  30861  dipass  30864  ip2eqi  30875  htth  30937  hvsubsub4  31079  hvnegdi  31086  hvaddcan  31089  hvaddcan2  31090  hvsubcan  31093  hvsubcan2  31094  hvaddsub4  31097  hial2eq  31125  normlem9at  31140  normsq  31153  norm-iii  31159  normsub  31162  normpyth  31164  normpar  31174  polid  31178  issubgoilem  31279  ococ  31425  chj0  31516  chlejb1  31531  chdmm1  31544  chjass  31552  spanun  31564  spansn  31578  elspansn2  31586  cmbr  31603  cmbr3  31627  pjoml2  31630  pjoml3  31631  osum  31664  spansnj  31666  pjch1  31689  pjadji  31704  pjaddi  31705  pjinormi  31706  pjsubi  31707  pjmuli  31708  pjcjt2  31711  pjch  31713  pjopyth  31739  pjpyth  31744  hoaddcom  31793  hoaddass  31801  hocsubdir  31804  hoaddrid  31810  ho0sub  31816  honegsub  31818  adjsym  31852  eigrei  31853  eigre  31854  eigposi  31855  eigorth  31857  ellnop  31877  elhmop  31892  ellnfn  31902  cnvadj  31911  lnopl  31933  unop  31934  hmop  31941  lnfnl  31950  adj1  31952  eleigvec  31976  hoddi  32009  lnopeq0lem2  32025  lnopunilem1  32029  lnopunilem2  32030  lnopunii  32031  elunop2  32032  lnophmi  32037  lnfnmul  32067  cnlnadjlem5  32090  branmfn  32124  bra11  32127  hmopidmchi  32170  hmopidmch  32172  hmopidmpj  32173  pjss2coi  32183  pjssmi  32184  pjssge0i  32185  pjidmco  32200  dfpjop  32201  elpjrn  32209  isst  32232  ishst  32233  hstel2  32238  stj  32254  mdbr  32313  mdi  32314  mdbr3  32316  dmdbr  32318  dmdmd  32319  dmdi  32321  dmdbr3  32324  mddmd2  32328  mdsl1i  32340  chjatom  32376  iuninc  32573  fmptcof2  32667  bcm1n  32797  fsumiunle  32831  xmulcand  32903  xrsmulgzz  33011  gsumle  33101  psgnfzto1st  33125  isslmd  33208  slmdlema  33209  gsumvsca1  33232  gsumvsca2  33233  urpropd  33236  elrgspnsubrunlem2  33252  erlval  33262  domnpropd  33280  domnlcanOLD  33283  qusvscpbl  33379  nsgqusf1olem3  33443  opprqusdrng  33521  ressply1mon1p  33593  ressply1invg  33594  ply1moneq  33611  fedgmul  33682  brfldext  33698  fldextrspunlsplem  33723  minplyval  33748  submateq  33808  dispcmp  33858  pstmxmet  33896  cnre2csqlem  33909  mndpluscn  33925  qqhval2  33983  isrrext  34001  esumfzf  34070  esumcvg  34087  esum2dlem  34093  esumiun  34095  ofcfeqd2  34102  ismeas  34200  isrnmeas  34201  measvun  34210  carsgval  34305  inelcarsg  34313  carsgclctunlem1  34319  carsgclctunlem2  34321  pmeasmono  34326  pmeasadd  34327  eulerpartlemgvv  34378  eulerpartlemn  34383  sseqp1  34397  probun  34421  sgnsgn  34551  breprexp  34648  istrkg2d  34681  axtgupdim2ALTV  34683  afsval  34686  bnj1385  34846  bnj66  34874  bnj106  34882  bnj155  34893  bnj222  34897  bnj540  34906  bnj591  34925  bnj594  34926  bnj611  34932  bnj893  34942  bnj1000  34955  bnj966  34958  bnj1112  34997  bnj1234  35027  bnj1253  35031  bnj1280  35034  bnj1326  35040  bnj1450  35064  bnj1463  35069  bnj1529  35084  f1resveqaeq  35099  pfxwlk  35129  revwlk  35130  subfacp1lem3  35187  subfacp1lem4  35188  subfacp1lem5  35189  subfacp1lem6  35190  subfacval2  35192  erdszelem9  35204  sconnpht  35234  ptpconn  35238  cvmliftmolem1  35286  cvmliftmolem2  35287  cvmliftlem10  35299  cvmlift2  35321  cvmliftphtlem  35322  satfdm  35374  gonarlem  35399  gonar  35400  goalr  35402  satfdmfmla  35405  prv  35433  mrsubff1  35519  mrsubccat  35523  elmrsubrn  35525  mrsubvrs  35527  elmpst  35541  msrid  35550  msubvrs  35565  sqdivzi  35728  shftvalg  35732  bcprod  35738  bccolsum  35739  iprodefisumlem  35740  faclimlem1  35743  rdgprc  35795  dfrdg2  35796  elwlim  35824  fvsingle  35921  fullfunfv  35948  lineelsb2  36149  rankung  36167  ranksng  36168  rankpwg  36170  opnregcld  36331  cldregopn  36332  neibastop3  36363  weiunlem1  36463  bj-sbeqALT  36901  bj-gabeqis  36939  bj-isclm  37292  rdgeqoa  37371  fvineqsnf1  37411  tan2h  37619  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem9  37636  poimirlem13  37640  poimirlem14  37641  poimirlem16  37643  poimirlem19  37646  broucube  37661  voliunnfl  37671  volsupnfl  37672  cocanfo  37726  upixp  37736  sdclem2  37749  caushft  37768  ismtycnv  37809  ismtyima  37810  ismtybndlem  37813  ismtyres  37815  bfplem2  37830  bfp  37831  isass  37853  opidonOLD  37859  exidu1  37863  cmpidelt  37866  grpoeqdivid  37888  elghomlem2OLD  37893  ghomlinOLD  37895  ghomco  37898  isrngo  37904  rngoid  37909  rngoideu  37910  rngodi  37911  rngodir  37912  rngoass  37913  rngohomval  37971  isrngohom  37972  rngohomadd  37976  rngohommul  37977  iscom2  38002  iscringd  38005  crngocom  38008  crngohomfo  38013  dmncan2  38084  elsymrels4  38556  brredunds  38627  lshpset  38979  lcvexchlem4  39038  lcvexchlem5  39039  lflset  39060  islfl  39061  lfli  39062  islfld  39063  eqlkr3  39102  isopos  39181  oposlem  39183  opcon3b  39197  cmtvalN  39212  omllaw  39244  cvlexchb2  39332  cvlatexchb2  39336  cvlsupr2  39344  4atlem9  39605  4atlem10a  39606  4atlem11a  39609  4atlem12a  39612  4at2  39616  pmapglb2N  39773  pmapglb2xN  39774  paddasslem17  39838  ispsubclN  39939  ispsubcl2N  39949  lhpmod2i2  40040  lhpmod6i1  40041  4atexlemex2  40073  4atex  40078  4atex2-0aOLDN  40080  4atex2-0cOLDN  40082  ldilval  40115  ltrnfset  40119  ltrnset  40120  isltrn  40121  ltrneq2  40150  trnfsetN  40157  trnsetN  40158  istrnN  40159  cdlemd5  40204  cdleme0moN  40227  cdleme0nex  40292  cdleme18d  40297  cdleme31so  40381  cdleme31fv  40392  cdlemg2jlemOLDN  40595  cdlemg2fvlem  40596  cdlemg2klem  40597  istendo  40762  tendovalco  40767  tendoeq2  40776  dicelvalN  41180  dihval  41234  dihcnv11  41277  dihmeetlem13N  41321  dihlspsnat  41335  dochn0nv  41377  dochkrshp4  41391  lpolsetN  41484  lpolsatN  41490  lpolpolsatN  41491  lcfl1lem  41493  lclkrlem2a  41509  lclkrlem2e  41513  lcfls1lem  41536  lclkrs2  41542  lcdfval  41590  lcdval  41591  mapdffval  41628  mapdfval  41629  mapd0  41667  mapdpglem30  41704  mapdhval  41726  mapdheq2  41731  hdmap1vallem  41799  hdmap1val  41800  hdmap1cbv  41804  hdmapval3N  41840  hdmap10  41842  hdmapeq0  41846  hdmap14lem12  41881  hdmap14lem13  41882  hgmapfval  41888  hgmapvs  41893  hgmapvv  41928  hlhilocv  41963  recbothd  41993  lcmineqlem13  42042  isprimroot  42094  primrootsunit1  42098  aks6d1c1p1  42108  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  evl1gprodd  42118  aks6d1c1rh  42126  aks6d1c2lem3  42127  deg1gprod  42141  deg1pow  42142  sticksstones22  42169  aks6d1c6lem2  42172  aks5lem3a  42190  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  ccatcan2d  42292  remulcan2d  42298  nnadd1com  42302  nnaddcom  42303  nnadddir  42305  nnmul1com  42306  nnmulcom  42307  sumcubes  42347  expeqidd  42360  efne0d  42373  cxp112d  42377  cxp111d  42378  log11d  42382  sn-addcand  42449  sn-addcan2d  42451  sn-mullid  42465  nn0addcom  42480  renegmulnnass  42483  nn0mulcom  42484  zmulcomlem  42485  cnreeu  42500  abvexp  42542  fiabv  42546  prjsprel  42614  prjcrvfval  42641  flt0  42647  sn-isghm  42683  ismrcd2  42710  ismrc  42712  dvdsrabdioph  42821  fphpdo  42828  rmxypairf1o  42923  monotoddzzfi  42954  monotoddzz  42955  oddcomabszz  42956  rmxdioph  43028  expdiophlem2  43034  dnnumch3  43059  aomclem8  43073  islssfg  43082  unxpwdom3  43107  gicabl  43111  idomodle  43203  fgraphxp  43216  hausgraph  43217  onov0suclim  43287  oaabsb  43307  oaomoencom  43330  oenass  43332  omabs2  43345  tfsconcat0b  43359  nadd1suc  43405  naddonnn  43408  minregex  43547  relexpmulnn  43722  clsk1independent  44059  ntrclsk13  44084  ntrclsk4  44085  imo72b2  44185  grumnud  44305  nzss  44336  caofcan  44342  expgrowth  44354  fsneq  45211  fperiodmullem  45315  uzinico3  45576  fsumf1of  45589  fmuldfeq  45598  fprodexp  45609  fprodabs2  45610  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climaddf  45630  mullimc  45631  limcperiod  45643  neglimc  45662  addlimc  45663  0ellimcdiv  45664  climeldmeqmpt  45683  climfveqmpt  45686  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  climeqf  45703  climeldmeqmpt3  45704  limsupequz  45738  cncfperiod  45894  icccncfext  45902  fperdvper  45934  dvnmptdivc  45953  dvnxpaek  45957  dvnmul  45958  dvmptfprod  45960  dvnprodlem3  45963  itgspltprt  45994  stoweidlem30  46045  stoweidlem48  46063  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  fourierdlem50  46171  fourierdlem73  46194  fourierdlem81  46202  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem94  46215  fourierdlem97  46218  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  sge0iunmptlemfi  46428  ismea  46466  meadjuni  46472  meaiuninclem  46495  caragenval  46508  isome  46509  caragensplit  46515  carageniuncllem1  46536  caratheodorylem1  46541  hoidmvlelem3  46612  vonvolmbllem  46675  vonvolmbl  46676  smflimlem3  46788  smflim  46792  smfpimcc  46823  smfsuplem2  46827  fsetsnf1  47064  cfsetsnfsetf1  47071  fcoresf1  47081  csbafv12g  47149  csbaovg  47192  csbafv212g  47231  fargshiftf1  47428  fargshiftfva  47430  prproropf1olem4  47493  fmtnorec2  47530  fmtnoprmfac1lem  47551  fmtnofac1  47557  quad1  47607  requad1  47609  perfectALTV  47710  fpprwppr  47726  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  sbgoldbo  47774  isgrim  47868  isuspgrim0  47872  grimuhgr  47878  grimcnv  47879  grimco  47880  gricushgr  47886  isubgrgrim  47897  uhgrimisgrgriclem  47898  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  uspgrlimlem3  47957  uspgrlimlem4  47958  grlimgrtrilem2  47962  gpgvtxedg0  48021  gpgvtxedg1  48022  uspgrsprf1  48063  plusfreseq  48080  iscomlaw  48106  isasslaw  48108  lidldomn1  48147  zlidlring  48150  rngcsectALTV  48191  ringcsectALTV  48225  ovmpordxf  48255  lmodvsmdi  48295  islininds  48363  lindslinindimp2lem4  48378  lindslinindsimp2  48380  lmod1  48409  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdig  48544  1arymaptf1  48563  2arymaptf1  48574  itcovalpc  48593  itcovalt2  48598  rrx2pnecoorneor  48636  rrx2plordisom  48644  rrx2line  48661  rrx2linest  48663  line2ylem  48672  line2x  48675  line2y  48676  itscnhlc0yqe  48680  itscnhlc0xyqsol  48686  idmon  48908  idepi  48909  fucofvalne  49020  grptcmon  49190  grptcepi  49191  aacllem  49320