Theorem eqeq12d 2785

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 2783	. 2 ⊢ ((𝜑 ∧ 𝜑) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	anidms 576	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  neeq12d  3025  cdeqeq  3747  sbceqg  4383  csbun  4412  csbin  4413  csbdif  4491  csbif  4550  iununi  5069  csbopab  5541  csbopabw  5542  dfid2  5559  csbima12  6082  dmsnsnsn  6222  csbcog  6299  dfpred3g  6315  preddowncl  6334  limeq  6373  csbiota  6530  fveqres  6926  opabiota  6964  fvmptf  7012  eqfnfv2f  7030  fsneq  7031  fvreseq0  7034  fveqdmss  7074  fvcofneq  7089  fnressn  7156  fnelfp  7174  fprb  7193  fnprb  7207  fntpb  7208  f1cofveqaeqALT  7257  nvocnv  7280  cocan1  7290  cocan2  7291  2fvcoidd  7296  fliftfun  7311  weniso  7353  csbriota  7383  oveqrspc2v  7438  csbov123  7455  eqfnov  7540  ovmpos  7559  ov2gf  7560  ovmpodxf  7561  caovcomg  7606  caovassg  7609  caovcang  7612  caovcanrd  7614  caovcan  7615  caovdig  7625  caovdirg  7628  caovmo  7648  coof  7699  offveqb  7702  caofid0l  7708  caofid0r  7709  caofidlcan  7713  caofass  7715  caonncan  7719  ordunisuc  7827  onsucuni2  7829  orduninsuc  7838  op1stg  7997  op2ndg  7998  f1o2ndf1  8116  xpord2pred  8140  xpord3pred  8147  poseq  8153  soseq  8154  fnsuppres  8186  csbfrecsg  8280  fpr3g  8281  frrlem1  8282  frrlem12  8293  frrlem13  8294  fpr2a  8298  wfr3g  8315  onfununi  8327  tfrlem1  8361  tfrlem3a  8362  tfrlem5  8365  tfrlem9  8371  tfrlem11  8374  tfrlem12  8375  tfr3  8385  tz7.44-1  8392  tz7.44-2  8393  tz7.44-3  8394  rdglem1  8401  rdg0g  8413  seqomlem1  8436  oalim  8516  omlim  8517  oelim  8518  oa0r  8522  om0r  8523  om1r  8527  oaass  8545  oarec  8546  odi  8563  omass  8564  oelim2  8580  oeoalem  8581  oeoa  8582  oeoelem  8583  oeoe  8584  nna0r  8594  nnacom  8602  nnaass  8607  nndi  8608  nnmass  8609  nnmsucr  8610  nnmcom  8611  oaabs  8633  oaabs2  8634  omabs  8636  naddcllem  8661  naddcom  8668  naddrid  8669  naddass  8682  naddsuc2  8687  naddoa  8688  ecovcom  8820  ecovass  8821  ecovdi  8822  dom2lem  8988  unxpdomlem2  9216  unxpdomlem3  9217  ixpfi2  9306  fipreima  9314  ordiso2  9476  wemaplem1  9507  wemaplem2  9508  wemapsolem  9511  cantnfval2  9637  cantnfp1lem3  9648  oemapvali  9652  cantnflem1c  9655  cantnflem1  9657  wemapwe  9665  rnttrcl  9690  tcvalg  9704  frr3g  9727  frr2  9731  rankvalg  9788  rankonidlem  9799  ranklim  9815  rankuni  9834  updjud  9919  cardprclem  9964  cardprc  9965  carduni  9966  fseqenlem1  10007  fodomacn  10039  alephcard  10053  alephfp2  10092  alephval3  10093  dfac12lem1  10126  dfac12lem2  10127  dfac12r  10129  ackbij1lem8  10208  ackbij1lem14  10214  ackbij1lem16  10216  ackbij2lem3  10222  cardcf  10234  sornom  10260  fin23lem28  10323  isf32lem2  10337  itunitc  10404  ituniiun  10405  axdc3lem2  10434  axdc4lem  10438  ttukeylem3  10494  ttukey2g  10499  fpwwe2lem7  10621  fpwwecbv  10628  canth4  10631  pwfseqlem2  10643  addcanpi  10883  mulcanpi  10884  recrecnq  10951  ltexnq  10959  genpv  10983  0idsr  11081  1idsr  11082  ax1rid  11145  mulrid  11205  addcan  11393  addcan2  11394  mulcand  11846  mulcan2d  11847  mulcan2g  11867  divmuleq  11919  conjmul  11931  eqneg  11934  ofsubeq0  12214  nnadd1com  12258  nnaddcom  12259  nnadddir  12291  nnmul1com  12292  nnmulcom  12293  rpnnen1lem6  13005  cnref1o  13008  xmulasslem  13310  xmulass  13312  xadddi2  13322  prunioo  13507  fzsuc2  13609  fzprval  13612  fztpval  13613  fzosplitprm1  13806  modadd1  13940  modaddb  13941  modmul1  13959  addmodlteq  13981  om2uzsuci  13983  om2uzrdg  13991  uzrdgxfr  14002  seq1  14049  seqp1  14051  seqfveq2  14059  seqfveq  14061  seqshft2  14063  seqsplit  14070  seqcaopr3  14072  seqcaopr2  14073  seqf1olem2a  14075  seqf1olem2  14077  seqf1o  14078  seqid  14082  seqid2  14083  seqhomo  14084  ser1const  14093  seqof2  14095  mulexp  14136  expadd  14139  expmul  14142  binom2  14252  sq01  14260  modexp  14273  bcpasc  14356  hashgadd  14412  hashdom  14414  hashfzo  14465  hashfzp1  14467  hashxplem  14469  hashxp  14470  hashmap  14471  hashpw  14472  hashbclem  14488  hashbc  14489  hashfacen  14490  hashf1lem1  14491  hashf1lem2  14492  hashf1  14493  seqcoll  14500  eqs1  14649  swrdspsleq  14702  pfxeq  14732  pfxsuff1eqwrdeq  14735  ccatopth2  14753  cats1un  14757  swrdccatin1  14761  swrdccat3blem  14775  cshf1  14846  repswcshw  14848  s2eq2s1eq  14972  s3eqs2s1eq  14974  pfx2  14983  2swrd2eqwrdeq  14989  wwlktovf1  14993  eqwrds3  14997  relexpsucnnr  15061  relexpsucnnl  15066  relexpcnv  15071  relexpaddnn  15087  replim  15166  cjreb  15173  cjexp  15200  absexp  15354  abs1m  15386  recan  15387  cnsqrt00  15443  isercoll2  15719  iseraltlem2  15733  iseraltlem3  15734  sumeq2ii  15743  zsum  15768  fsum  15770  fsumf1o  15773  sumss  15774  fsumcvg2  15777  fsumadd  15790  isummulc2  15812  fsum2d  15821  fsummulc2  15834  fsumconst  15840  modfsummods  15844  modfsummod  15845  fsumparts  15857  fsumrelem  15858  fsumiun  15872  binom  15883  bcxmas  15888  incexclem  15889  isumshft  15892  isumnn0nn  15895  climcndslem1  15902  climcndslem2  15903  mertenslem2  15938  clim2prod  15941  prodfrec  15948  prodeq2ii  15964  zprod  15990  fprod  15994  fprodf1o  15999  fprodser  16002  fprodmul  16013  fproddiv  16014  prodsn  16015  prodsnf  16017  fprodabs  16027  fprodconst  16031  fprod2d  16034  fprodmodd  16050  binomfallfac  16094  bpolydif  16108  fprodefsum  16148  efne0d  16150  efne0OLD  16152  efexp  16156  demoivreALT  16256  moddvds  16320  bitsinv1  16499  sadadd2  16517  smu01lem  16542  smupval  16545  smueqlem  16547  smumullem  16549  gcdaddm  16582  bezoutlem1  16596  bezout  16600  gcddiv  16608  seq1st  16628  alginv  16632  algfx  16637  lcmneg  16660  lcmid  16666  lcmgcdeq  16669  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfunsnlem  16698  lcmfunsn  16701  lcmfun  16702  divgcdcoprm0  16722  cncongr1  16724  cncongr2  16725  nn0gcdsq  16810  crth  16836  eulerthlem2  16840  pythagtriplem1  16875  iserodd  16894  pcqmul  16912  pcexp  16918  pcneg  16933  pcmpt  16951  pcfac  16958  prmreclem2  16976  prmreclem3  16977  1arith  16986  vdwpc  17039  ramcl  17088  prmop1  17097  imasval  17564  ercpbllem  17601  iscat  17727  iscatd  17728  catideu  17730  iscatd2  17736  catlid  17738  catrid  17739  catass  17741  homfeq  17749  comfeq  17761  catpropd  17764  moni  17792  epii  17799  sectffval  17806  sectfval  17807  oppcsect  17834  sectmon  17838  isfunc  17920  funcid  17926  funcco  17927  funcpropd  17958  isfull  17968  fthsect  17983  fthmon  17985  natfval  18005  isnat  18006  nati  18014  fucsect  18031  natpropd  18035  setcmon  18143  setcepi  18144  setcsect  18145  fthestrcsetc  18205  embedsetcestrclem  18212  fthsetcestrc  18220  evlfcl  18277  uncfcurf  18294  yoniso  18340  joinval  18430  meetval  18444  islat  18488  latdisdlem  18551  latdisd  18552  isclat  18555  isdlat  18577  dlatmjdi  18578  isacs5lem  18600  acsdrscl  18601  acsficl  18602  isps  18623  mgmidmo  18717  mgmlrid  18724  lidrideqd  18726  lidrididd  18727  grpinvalem  18730  grpinva  18731  gsumvalx  18733  gsumval2  18743  ismgmhm  18753  mgmhmpropd  18755  mgmhmlin  18756  mgmhmeql  18773  issgrp  18777  isnsgrp  18780  sgrpass  18782  sgrp1  18786  issgrpd  18787  sgrppropd  18788  ismndd  18813  mndpropd  18816  imasmnd2  18831  xpsmnd0  18835  mnd1  18836  mnd1id  18837  ismhm  18842  mhmpropd  18849  mhmlin  18850  mhmimalem  18882  mhmeql  18884  gsumccat  18899  gsumwmhm  18903  frmdgsum  18920  symggrplem  18942  smndex1mndlem  18970  smndex1n0mnd  18973  sgrp2rid2  18987  sgrp2nmndlem4  18989  isgrp  19005  grppropd  19017  isgrpd2e  19021  dfgrp2  19028  isgrpid2  19042  grpidd2  19043  grpinvfval  19044  grpinvfvalALT  19045  grpinv11  19073  grpinvpropd  19080  grpidssd  19081  grpinvssd  19082  grpsubrcan  19086  dfgrp3lem  19103  grplactcnv  19108  imasgrp2  19120  mhmlem  19127  mulgnn0p1  19150  mulgaddcom  19163  mulginvcom  19164  mulgneg2  19173  mulgnnass  19174  mulgnn0ass  19175  mulgass  19176  mhmmulg  19180  cyccom  19273  isghm  19285  ghmlin  19290  ghmeql  19308  isga  19360  gagrpid  19363  gaass  19366  galcan  19373  orbsta  19382  cntzfval  19389  elcntz  19391  cntzsnval  19393  elcntzsn  19394  cntzi  19398  resscntz  19402  cntzmhm  19410  gsumwrev  19435  snsymgefmndeq  19464  cayleylem2  19482  symgextf1  19490  gsmsymgreqlem2  19500  gsmsymgreq  19501  symgfixf1  19506  pmtrfrn  19527  odfval  19601  odfvalALT  19602  mndodcong  19611  odbezout  19627  odeq1  19629  submod  19638  gexval  19647  gexdvds  19653  ispgp  19661  sylow1lem1  19667  sylow2alem1  19686  sylow2alem2  19687  sylow2blem2  19690  efgmnvl  19783  efgredlemc  19814  efgredeu  19821  frgpuptinv  19840  frgpup1  19844  frgpup3lem  19846  iscmn  19858  cmnpropd  19860  iscmnd  19863  abladdsub4  19880  submcmn2  19908  qusabl  19934  abl1  19935  imasabl  19945  iscyg  19948  cycsubmcmn  19958  gsum2dlem2  20040  telgsumfzs  20058  dmdprd  20069  dprdval  20074  dprdfcntz  20086  subgdmdprd  20105  dprd2da  20113  dpjrid  20133  pgpfac1lem3a  20147  ablfaclem3  20158  ablfac2  20160  gsumle  20214  isrng  20231  rngdi  20237  rngdir  20238  rngpropd  20251  imasrng  20254  ringurd  20266  issrg  20269  o2timesd  20291  rglcom4d  20292  srgmulgass  20298  srgpcomp  20299  srgbinom  20312  isring  20318  ringpropd  20370  ringinvnz1ne0  20382  mulgass2  20391  ring1  20392  imasring  20411  xpsring1d  20414  dvdsr  20443  dvreq1  20492  rnghmval  20521  isrnghm  20522  rnghmmul  20530  c0snmgmhm  20543  rngisomring1  20549  zrrnghm  20620  islring  20624  rngcsect  20720  ringcsect  20754  rrgval  20781  unitrrg  20787  domnlcanb  20803  domnrcanb  20805  isdrng  20816  drngprop  20827  isdrngd  20846  isdrngdOLD  20848  drngpropd  20850  cntzsdrg  20882  isabv  20891  abvmul  20901  issrng  20924  issrngd  20935  idsrngd  20936  islmod  20962  lmodlema  20963  islmodd  20964  lmodvsmmulgdi  20995  lmodprop2d  21022  rmodislmodlem  21027  rmodislmod  21028  islmhm  21125  lmhmlin  21133  islmhm2  21136  lmhmeql  21153  lmhmpropd  21171  islbs  21174  lbspropd  21197  rnglidlmsgrp  21353  rnglidlrng  21354  quscrng  21393  rngqiprngimfo  21411  islpir  21464  cnfldmulg  21522  cnfldexp  21523  prmirredlem  21590  pzriprnglem6  21604  pzriprnglem10  21608  pzriprnglem12  21610  chrcong  21645  zndvds  21667  znf1o  21669  znunit  21681  cygznlem3  21687  frgpcyg  21691  psgndiflemB  21718  isphl  21746  ipcj  21752  iporthcom  21753  ip2eq  21771  isphld  21772  phlpropd  21773  phlssphl  21777  ocvfval  21784  iscss  21801  ishil  21836  isobs  21838  obsip  21839  obslbs  21848  frlmphl  21899  isassa  21974  assalem  21975  isassad  21983  assapropd  21989  assamulgscm  22019  mvrf1  22103  mplmonmul  22155  mplcoe1  22156  mplcoe3  22157  mplcoe5lem  22158  mplcoe5  22159  evlslem1  22201  mpfrcl  22204  evlsval  22205  psdpw  22301  coe1tm  22402  ply1sclf1  22418  ply1coe  22426  eqcoe1ply1eq  22427  cply1coe0bi  22430  coe1fzgsumd  22432  ply1scleq  22433  ply1chr  22434  gsumply1eq  22437  evl1gsumd  22485  mat0dimcrng  22595  mat1ghm  22608  mat1mhm  22609  dmatcrng  22627  scmateALT  22637  scmatcrng  22646  scmatf1  22656  mvmumamul1  22679  mdetdiagid  22725  mdetralt  22733  mdetunilem1  22737  mdetunilem3  22739  mdetunilem4  22740  mdetunilem7  22743  mdetunilem9  22745  mdetuni0  22746  madugsum  22768  smadiadetr  22800  mat2pmatf1  22854  m2cpminvid2lem  22879  decpmataa0  22893  pmatcollpw2lem  22902  pm2mpf1  22924  chcoeffeqlem  23010  chcoeffeq  23011  cayhamlem3  23012  cayleyhamilton1  23017  isperf  23276  restperf  23309  cmpsub  23525  isconn  23538  2ndcsep  23584  elptr2  23699  ptbasin  23702  dfac14  23743  txcnp  23745  ptcnplem  23746  ptcnp  23747  cnmpt11  23788  cnmpt21  23796  cnmptcom  23803  kqfeq  23849  isr0  23862  pt1hmeo  23931  ustexsym  24341  isusp  24386  imasdsf1olem  24498  isxms  24572  xmspropd  24598  imasf1oxms  24614  stdbdmopn  24643  isngp3  24723  ngppropd  24762  tngngp3  24781  isnlm  24800  nmvs  24801  xrsxmet  24935  cnheibor  25082  htpyi  25101  htpycc  25107  pi1xfr  25182  pi1coghm  25188  isclm  25191  lmhmclm  25214  isclmp  25224  clmmulg  25228  iscph  25297  tcphcph  25364  cphsscph  25378  cmetcaulem  25415  bcth3  25458  ovolunlem1a  25623  ovolicc2lem1  25644  ovolicc2lem4  25647  ovolicc2  25649  mblsplit  25659  volun  25672  volfiniun  25674  voliunlem1  25677  volsup  25683  ioorinv  25703  uniioombllem2  25710  vitalilem3  25737  mbfeqalem1  25768  mbflim  25795  itgeqa  25941  itgconst  25946  itgfsum  25954  itgsplitioo  25965  dvnadd  26056  dvnres  26058  dvexp  26080  dvmptfsum  26102  mvth  26119  dvlip  26120  lhop1lem  26140  dvcvx  26147  mdegle0  26202  ply1nzb  26248  mon1pval  26267  facth1  26292  ig1pval  26301  dgrmulc  26396  dgrcolem1  26398  dgrcolem2  26399  dgrco  26400  coecj  26403  coecjOLD  26405  vieta1lem2  26440  vieta1  26441  elqaalem3  26450  dvntaylp  26499  ulmss  26525  mtest  26532  sineq0  26654  efif1olem4  26675  cxpexp  26798  mulcxplem  26814  mulcxp  26815  cxpmul2  26819  cxpeq  26887  affineequiv2  26954  quad2  26969  dcubic  26976  leibpi  27072  o1cxp  27104  scvxcvx  27115  facgam  27195  wilthlem1  27197  wilthlem2  27198  mpodvdsmulf1o  27323  fsumdvdsmul  27324  perfect  27360  dchrelbas2  27366  dchrinv  27390  dchrptlem2  27394  lgsne0  27464  lgsqrlem2  27476  lgsdchr  27484  gausslemma2d  27503  lgseisenlem2  27505  lgsquad2lem2  27514  2lgslem1a  27520  2lgslem1b  27521  dchrisumlem1  27618  qabvexp  27755  ostthlem1  27756  ostthlem2  27757  ostth3  27767  ltsval2  27785  ltsres  27791  nolesgn2ores  27801  nogesgn1ores  27803  nolt02o  27824  nogt01o  27825  nosupcbv  27831  nosupno  27832  nosupdm  27833  nosupfv  27835  nosupres  27836  nosupbnd1lem1  27837  nosupbnd1lem3  27839  nosupbnd1lem5  27841  noinfcbv  27846  noinfno  27847  noinfdm  27848  noinffv  27850  noinfres  27851  noinfbnd1lem3  27854  noinfbnd1lem5  27856  addsrid  28122  addscom  28124  addscan1  28152  addsass  28163  subscan1d  28261  subscan2d  28262  mulsrid  28271  mulscom  28297  addsdilem3  28311  addsdilem4  28312  addsdi  28313  mulsasslem3  28323  mulsass  28324  mulscan2d  28337  mulscan1d  28338  bdayons  28434  om2noseqrdg  28462  n0cut  28492  expadds  28593  pw2cut  28618  pw2cut2  28620  elreno  28649  istrkgc  28688  istrkgcb  28690  istrkgld  28693  istrkg2ld  28694  axtgcgrrflx  28696  axtgupdim2  28705  tgjustf  28707  tgjustr  28708  iscgrg  28746  iscgrglt  28748  trgcgrg  28749  tgcgr4  28765  motcgr  28770  legso  28833  mirval  28893  israg  28935  ismidb  29044  isinagd  29110  f1otrgds  29158  ttgval  29164  ttgitvval  29171  brcgr  29190  brbtwn2  29195  colinearalglem1  29196  colinearalg  29200  ax5seglem1  29218  ax5seglem2  29219  ax5seglem8  29226  ax5seglem9  29227  axlowdimlem13  29244  axlowdimlem16  29247  axlowdim1  29249  axcontlem1  29254  axcontlem2  29255  axcontlem6  29259  axcontlem7  29260  axcontlem8  29261  ecgrtg  29273  usgredg2v  29517  issubgr  29561  cplgruvtxb  29703  cusgrsize  29744  finsumvtxdg2size  29840  isrgr  29849  wkslem1  29897  wkslem2  29898  iswlk  29900  uspgr2wlkeq  29935  2wlklem  29955  wlkres  29958  redwlk  29960  wlkp1lem6  29966  wlkp1lem7  29967  wlkp1lem8  29968  pthdivtx  30016  upgrwlkdvdelem  30025  isclwlk  30062  iscrct  30079  iscycl  30080  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  wwlksnextinj  30188  rusgrnumwwlk  30267  clwlkclwwlklem2  30291  clwlkclwwlkf1lem3  30297  clwlkclwwlkf1  30301  erclwwlkeq  30309  clwwlkel  30337  clwwlkf  30338  clwwlkf1  30340  erclwwlkneq  30358  clwwlkvbij  30404  upgreupthseg  30500  eupth2eucrct  30508  eupth2lem3  30527  eupth2  30530  eucrctshift  30534  2clwwlk  30638  numclwwlk1lem2f1  30648  numclwlk1lem1  30660  numclwlk1lem2  30661  numclwlk2lem2f1o  30670  isgrpo  30789  grpoass  30795  grpoidinvlem3  30798  grpoidinv  30800  grpoideu  30801  grpoidinv2  30807  grpoinvfval  30814  isablo  30838  ablocom  30840  vciOLD  30853  vcidOLD  30856  vcdi  30857  vcdir  30858  vcass  30859  isvclem  30869  isnvlem  30902  nvmeq0  30950  nvs  30955  imsmetlem  30982  islno  31045  lnolin  31046  ishmo  31103  isphg  31109  phpar2  31115  phpar  31116  ipdiri  31122  ipasslem1  31123  ipasslem5  31127  ipasslem11  31132  ipassi  31133  dipdir  31134  dipass  31137  ip2eqi  31148  htth  31210  hvsubsub4  31352  hvnegdi  31359  hvaddcan  31362  hvaddcan2  31363  hvsubcan  31366  hvsubcan2  31367  hvaddsub4  31370  hial2eq  31398  normlem9at  31413  normsq  31426  norm-iii  31432  normsub  31435  normpyth  31437  normpar  31447  polid  31451  issubgoilem  31552  ococ  31698  chj0  31789  chlejb1  31804  chdmm1  31817  chjass  31825  spanun  31837  spansn  31851  elspansn2  31859  cmbr  31876  cmbr3  31900  pjoml2  31903  pjoml3  31904  osum  31937  spansnj  31939  pjch1  31962  pjadji  31977  pjaddi  31978  pjinormi  31979  pjsubi  31980  pjmuli  31981  pjcjt2  31984  pjch  31986  pjopyth  32012  pjpyth  32017  hoaddcom  32066  hoaddass  32074  hocsubdir  32077  hoaddrid  32083  ho0sub  32089  honegsub  32091  adjsym  32125  eigrei  32126  eigre  32127  eigposi  32128  eigorth  32130  ellnop  32150  elhmop  32165  ellnfn  32175  cnvadj  32184  lnopl  32206  unop  32207  hmop  32214  lnfnl  32223  adj1  32225  eleigvec  32249  hoddi  32282  lnopeq0lem2  32298  lnopunilem1  32302  lnopunilem2  32303  lnopunii  32304  elunop2  32305  lnophmi  32310  lnfnmul  32340  cnlnadjlem5  32363  branmfn  32397  bra11  32400  hmopidmchi  32443  hmopidmch  32445  hmopidmpj  32446  pjss2coi  32456  pjssmi  32457  pjssge0i  32458  pjidmco  32473  dfpjop  32474  elpjrn  32482  isst  32505  ishst  32506  hstel2  32511  stj  32527  mdbr  32586  mdi  32587  mdbr3  32589  dmdbr  32591  dmdmd  32592  dmdi  32594  dmdbr3  32597  mddmd2  32601  mdsl1i  32613  chjatom  32649  iuninc  32845  fmptcof2  32942  receqid  33029  bcm1n  33080  fsumiunle  33113  sgnsgn  33115  xmulcand  33180  xrsmulgzz  33269  psgnfzto1st  33365  isfxp  33428  fxpgaeq  33429  isslmd  33462  slmdlema  33463  gsumvsca1  33486  gsumvsca2  33487  urpropd  33490  elrgspnsubrunlem2  33508  erlval  33518  domnpropd  33540  qusvscpbl  33613  nsgqusf1olem3  33667  opprqusdrng  33719  ressply1mon1p  33802  ressply1invg  33803  deg1prod  33817  ply1moneq  33822  psrgsum  33882  psrmonmul  33884  psrmonprod  33886  vietalem  33913  vieta  33914  fedgmul  33965  brfldext  33979  fldextrspunlsplem  34007  extdgfialglem1  34026  bralgext  34031  minplyval  34039  submateq  34143  dispcmp  34193  pstmxmet  34231  cnre2csqlem  34244  mndpluscn  34260  qqhval2  34316  isrrext  34334  esumfzf  34403  esumcvg  34420  esum2dlem  34426  esumiun  34428  ofcfeqd2  34435  ismeas  34533  isrnmeas  34534  measvun  34543  carsgval  34637  inelcarsg  34645  carsgclctunlem1  34651  carsgclctunlem2  34653  pmeasmono  34658  pmeasadd  34659  eulerpartlemgvv  34710  eulerpartlemn  34715  sseqp1  34729  probun  34753  breprexp  34964  istrkg2d  34997  axtgupdim2ALTV  34999  afsval  35005  bnj1385  35164  bnj66  35192  bnj106  35200  bnj155  35211  bnj222  35215  bnj540  35224  bnj591  35243  bnj594  35244  bnj611  35250  bnj893  35260  bnj1000  35273  bnj966  35276  bnj1112  35315  bnj1234  35345  bnj1253  35349  bnj1280  35352  bnj1326  35358  bnj1450  35382  bnj1463  35387  bnj1529  35402  f1resveqaeq  35416  pfxwlk  35514  revwlk  35515  subfacp1lem3  35572  subfacp1lem4  35573  subfacp1lem5  35574  subfacp1lem6  35575  subfacval2  35577  erdszelem9  35589  sconnpht  35619  ptpconn  35623  cvmliftmolem1  35671  cvmliftmolem2  35672  cvmliftlem10  35684  cvmlift2  35706  cvmliftphtlem  35707  satfdm  35759  gonarlem  35784  gonar  35785  goalr  35787  satfdmfmla  35790  prv  35818  mrsubff1  35904  mrsubccat  35908  elmrsubrn  35910  mrsubvrs  35912  elmpst  35926  msrid  35935  msubvrs  35950  sqdivzi  36118  shftvalg  36122  bcprod  36128  bccolsum  36129  iprodefisumlem  36130  faclimlem1  36133  rdgprc  36182  dfrdg2  36183  elwlim  36211  fvsingle  36308  fullfunfv  36337  lineelsb2  36538  rankung  36556  ranksng  36557  rankpwg  36559  nmulprop  36580  nmulcom  36584  opnregcld  36729  cldregopn  36730  neibastop3  36761  weiunval  36861  csbttc  36908  mh-inf3f1  36940  bj-sbeqALT  37423  bj-gabeqis  37461  bj-isclm  37822  rdgeqoa  37903  fvineqsnf1  37943  tan2h  38150  matunitlindflem1  38154  matunitlindflem2  38155  poimirlem9  38167  poimirlem13  38171  poimirlem14  38172  poimirlem16  38174  poimirlem19  38177  broucube  38192  voliunnfl  38202  volsupnfl  38203  cocanfo  38257  upixp  38267  sdclem2  38280  caushft  38299  ismtycnv  38340  ismtyima  38341  ismtybndlem  38344  ismtyres  38346  bfplem2  38361  bfp  38362  isass  38384  opidonOLD  38390  exidu1  38394  cmpidelt  38397  grpoeqdivid  38419  elghomlem2OLD  38424  ghomlinOLD  38426  ghomco  38429  isrngo  38435  rngoid  38440  rngoideu  38441  rngodi  38442  rngodir  38443  rngoass  38444  rngohomval  38502  isrngohom  38503  rngohomadd  38507  rngohommul  38508  iscom2  38533  iscringd  38536  crngocom  38539  crngohomfo  38544  dmncan2  38615  elsymrels4  39177  brredunds  39248  lshpset  39641  lcvexchlem4  39700  lcvexchlem5  39701  lflset  39722  islfl  39723  lfli  39724  islfld  39725  eqlkr3  39764  isopos  39843  oposlem  39845  opcon3b  39859  cmtvalN  39874  omllaw  39906  cvlexchb2  39994  cvlatexchb2  39998  cvlsupr2  40006  4atlem9  40266  4atlem10a  40267  4atlem11a  40270  4atlem12a  40273  4at2  40277  pmapglb2N  40434  pmapglb2xN  40435  paddasslem17  40499  ispsubclN  40600  ispsubcl2N  40610  lhpmod2i2  40701  lhpmod6i1  40702  4atexlemex2  40734  4atex  40739  4atex2-0aOLDN  40741  4atex2-0cOLDN  40743  ldilval  40776  ltrnfset  40780  ltrnset  40781  isltrn  40782  ltrneq2  40811  trnfsetN  40818  trnsetN  40819  istrnN  40820  cdlemd5  40865  cdleme0moN  40888  cdleme0nex  40953  cdleme18d  40958  cdleme31so  41042  cdleme31fv  41053  cdlemg2jlemOLDN  41256  cdlemg2fvlem  41257  cdlemg2klem  41258  istendo  41423  tendovalco  41428  tendoeq2  41437  dicelvalN  41841  dihval  41895  dihcnv11  41938  dihmeetlem13N  41982  dihlspsnat  41996  dochn0nv  42038  dochkrshp4  42052  lpolsetN  42145  lpolsatN  42151  lpolpolsatN  42152  lcfl1lem  42154  lclkrlem2a  42170  lclkrlem2e  42174  lcfls1lem  42197  lclkrs2  42203  lcdfval  42251  lcdval  42252  mapdffval  42289  mapdfval  42290  mapd0  42328  mapdpglem30  42365  mapdhval  42387  mapdheq2  42392  hdmap1vallem  42460  hdmap1val  42461  hdmap1cbv  42465  hdmapval3N  42501  hdmap10  42503  hdmapeq0  42507  hdmap14lem12  42542  hdmap14lem13  42543  hgmapfval  42549  hgmapvs  42554  hgmapvv  42589  hlhilocv  42620  recbothd  42648  lcmineqlem13  42697  isprimroot  42749  primrootsunit1  42753  aks6d1c1p1  42763  aks6d1c1p3  42766  aks6d1c1p4  42767  aks6d1c1p5  42768  evl1gprodd  42773  aks6d1c1rh  42781  aks6d1c2lem3  42782  deg1gprod  42796  deg1pow  42797  sticksstones22  42824  aks6d1c6lem2  42827  aks5lem3a  42845  unitscyglem2  42852  unitscyglem3  42853  unitscyglem4  42854  ccatcan2d  42908  remulcan2d  42913  sumcubes  42963  expeqidd  42975  cxp112d  42991  cxp111d  42992  log11d  42996  sn-addcand  43070  sn-addcan2d  43072  sn-mullid  43086  nn0addcom  43125  renegmulnnass  43128  nn0mulcom  43129  zmulcomlem  43130  cnreeu  43153  abvexp  43191  fiabv  43195  prjsprel  43227  prjcrvfval  43254  flt0  43260  sn-isghm  43296  ismrcd2  43321  ismrc  43323  dvdsrabdioph  43428  fphpdo  43435  rmxypairf1o  43529  monotoddzzfi  43560  monotoddzz  43561  oddcomabszz  43562  rmxdioph  43634  expdiophlem2  43640  dnnumch3  43665  aomclem8  43679  islssfg  43688  unxpwdom3  43713  gicabl  43717  idomodle  43809  fgraphxp  43822  hausgraph  43823  onov0suclim  43892  oaabsb  43912  oaomoencom  43935  oenass  43937  omabs2  43950  tfsconcat0b  43964  nadd1suc  44010  naddonnn  44013  minregex  44151  relexpmulnn  44326  clsk1independent  44663  ntrclsk13  44688  ntrclsk4  44689  imo72b2  44789  grumnud  44887  nzss  44918  caofcan  44924  expgrowth  44936  fperiodmullem  45913  uzinico3  46169  fsumf1of  46181  fmuldfeq  46190  fprodexp  46201  fprodabs2  46202  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climaddf  46222  mullimc  46223  limcperiod  46235  neglimc  46252  addlimc  46253  0ellimcdiv  46254  climeldmeqmpt  46273  climfveqmpt  46276  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  climeqf  46293  climeldmeqmpt3  46294  limsupequz  46328  cncfperiod  46484  icccncfext  46492  fperdvper  46524  dvnmptdivc  46543  dvnxpaek  46547  dvnmul  46548  dvmptfprod  46550  dvnprodlem3  46553  itgspltprt  46584  stoweidlem30  46635  stoweidlem48  46653  wallispilem4  46673  wallispi2lem1  46676  wallispi2lem2  46677  fourierdlem50  46761  fourierdlem73  46784  fourierdlem81  46792  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem92  46803  fourierdlem94  46805  fourierdlem97  46808  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  sge0iunmptlemfi  47018  ismea  47056  meadjuni  47062  meaiuninclem  47085  caragenval  47098  isome  47099  caragensplit  47105  carageniuncllem1  47126  caratheodorylem1  47131  hoidmvlelem3  47202  vonvolmbllem  47265  vonvolmbl  47266  smflimlem3  47378  smflim  47382  smfpimcc  47413  smfsuplem2  47417  fsetsnf1  47677  cfsetsnfsetf1  47684  fcoresf1  47694  csbafv12g  47762  csbaovg  47805  csbafv212g  47844  mod2addne  47995  fargshiftf1  48078  fargshiftfva  48080  prproropf1olem4  48143  fmtnorec2  48183  fmtnoprmfac1lem  48204  fmtnofac1  48210  quad1  48273  requad1  48275  perfectALTV  48376  fpprwppr  48392  nfermltl8rev  48395  nfermltl2rev  48396  nfermltlrev  48397  sbgoldbo  48440  isgrim  48535  grimuhgr  48540  grimcnv  48541  grimco  48542  uhgrimedgi  48543  isuspgrim0  48547  upgrimwlklem5  48554  gricushgr  48570  isubgrgrim  48582  uhgrimisgrgriclem  48583  clnbgrgrimlem  48586  clnbgrgrim  48587  grimedg  48588  uspgrlimlem3  48643  uspgrlimlem4  48644  grlimedgclnbgr  48648  grlimgrtrilem2  48655  gpgvtxedg0  48716  gpgvtxedg1  48717  uspgrsprf1  48800  plusfreseq  48817  iscomlaw  48843  isasslaw  48845  lidldomn1  48884  zlidlring  48887  rngcsectALTV  48928  ringcsectALTV  48962  ovmpordxf  49003  lmodvsmdi  49043  islininds  49110  lindslinindimp2lem4  49125  lindslinindsimp2  49127  lmod1  49156  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  nn0sumshdiglem1  49285  nn0sumshdig  49287  1arymaptf1  49306  2arymaptf1  49317  itcovalpc  49336  itcovalt2  49341  rrx2pnecoorneor  49379  rrx2plordisom  49387  rrx2line  49404  rrx2linest  49406  line2ylem  49415  line2x  49418  line2y  49419  itscnhlc0yqe  49423  itscnhlc0xyqsol  49429  idmon  49682  idepi  49683  sectpropdlem  49698  ssccatid  49734  imaidfu  49772  oppff1  49810  imasubc  49813  diag1f1lem  49968  diag2f1lem  49970  fucofvalne  49987  catcsect  50060  grptcmon  50255  grptcepi  50256  aacllem  50474