Theorem eqeq12d 2752

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  neeq12d  2993  cdeqeq  3721  sbceqg  4352  csbun  4381  csbin  4382  csbdif  4465  csbif  4524  iununi  5041  csbopab  5510  csbopabgALT  5511  dfid2  5528  csbima12  6044  dmsnsnsn  6184  csbcog  6261  dfpred3g  6277  preddowncl  6296  limeq  6335  csbiota  6491  fveqres  6884  opabiota  6922  fvmptf  6969  eqfnfv2f  6987  fvreseq0  6990  fveqdmss  7030  fvcofneq  7045  fnressn  7112  fnelfp  7130  fprb  7149  fnprb  7163  fntpb  7164  f1cofveqaeqALT  7213  nvocnv  7236  cocan1  7246  cocan2  7247  2fvcoidd  7252  fliftfun  7267  weniso  7309  csbriota  7339  oveqrspc2v  7394  csbov123  7411  eqfnov  7496  ovmpos  7515  ov2gf  7516  ovmpodxf  7517  caovcomg  7562  caovassg  7565  caovcang  7568  caovcanrd  7570  caovcan  7571  caovdig  7581  caovdirg  7584  caovmo  7604  coof  7655  offveqb  7658  caofid0l  7664  caofid0r  7665  caofidlcan  7669  caofass  7671  caonncan  7675  ordunisuc  7783  onsucuni2  7785  orduninsuc  7794  op1stg  7954  op2ndg  7955  f1o2ndf1  8072  xpord2pred  8095  xpord3pred  8102  poseq  8108  soseq  8109  fnsuppres  8141  csbfrecsg  8234  fpr3g  8235  frrlem1  8236  frrlem12  8247  frrlem13  8248  fpr2a  8252  wfr3g  8269  onfununi  8281  tfrlem1  8315  tfrlem3a  8316  tfrlem5  8319  tfrlem9  8324  tfrlem11  8327  tfrlem12  8328  tfr3  8338  tz7.44-1  8345  tz7.44-2  8346  tz7.44-3  8347  rdglem1  8354  rdg0g  8366  seqomlem1  8389  oalim  8467  omlim  8468  oelim  8469  oa0r  8473  om0r  8474  om1r  8478  oaass  8496  oarec  8497  odi  8514  omass  8515  oelim2  8531  oeoalem  8532  oeoa  8533  oeoelem  8534  oeoe  8535  nna0r  8545  nnacom  8553  nnaass  8558  nndi  8559  nnmass  8560  nnmsucr  8561  nnmcom  8562  oaabs  8584  oaabs2  8585  omabs  8587  naddcllem  8612  naddcom  8618  naddrid  8619  naddass  8632  naddsuc2  8637  naddoa  8638  ecovcom  8770  ecovass  8771  ecovdi  8772  dom2lem  8939  unxpdomlem2  9167  unxpdomlem3  9168  ixpfi2  9260  fipreima  9268  ordiso2  9430  wemaplem1  9461  wemaplem2  9462  wemapsolem  9465  cantnfval2  9590  cantnfp1lem3  9601  oemapvali  9605  cantnflem1c  9608  cantnflem1  9610  wemapwe  9618  rnttrcl  9643  tcvalg  9657  frr3g  9680  frr2  9684  rankvalg  9741  rankonidlem  9752  ranklim  9768  rankuni  9787  updjud  9858  cardprclem  9903  cardprc  9904  carduni  9905  fseqenlem1  9946  fodomacn  9978  alephcard  9992  alephfp2  10031  alephval3  10032  dfac12lem1  10066  dfac12lem2  10067  dfac12r  10069  ackbij1lem8  10148  ackbij1lem14  10154  ackbij1lem16  10156  ackbij2lem3  10162  cardcf  10174  sornom  10199  fin23lem28  10262  isf32lem2  10276  itunitc  10343  ituniiun  10344  axdc3lem2  10373  axdc4lem  10377  ttukeylem3  10433  ttukey2g  10438  fpwwe2lem7  10560  fpwwecbv  10567  canth4  10570  pwfseqlem2  10582  addcanpi  10822  mulcanpi  10823  recrecnq  10890  ltexnq  10898  genpv  10922  0idsr  11020  1idsr  11021  ax1rid  11084  mulrid  11142  addcan  11330  addcan2  11331  mulcand  11783  mulcan2d  11784  mulcan2g  11804  div11OLD  11838  divmuleq  11860  conjmul  11872  eqneg  11875  ofsubeq0  12156  nnadd1com  12200  nnaddcom  12201  nnadddir  12233  nnmul1com  12234  nnmulcom  12235  rpnnen1lem6  12932  cnref1o  12935  xmulasslem  13237  xmulass  13239  xadddi2  13249  prunioo  13434  fzsuc2  13536  fzprval  13539  fztpval  13540  fzosplitprm1  13733  modadd1  13867  modaddb  13868  modmul1  13886  addmodlteq  13908  om2uzsuci  13910  om2uzrdg  13918  uzrdgxfr  13929  seq1  13976  seqp1  13978  seqfveq2  13986  seqfveq  13988  seqshft2  13990  seqsplit  13997  seqcaopr3  13999  seqcaopr2  14000  seqf1olem2a  14002  seqf1olem2  14004  seqf1o  14005  seqid  14009  seqid2  14010  seqhomo  14011  ser1const  14020  seqof2  14022  mulexp  14063  expadd  14066  expmul  14069  binom2  14179  sq01  14187  modexp  14200  bcpasc  14283  hashgadd  14339  hashdom  14341  hashfzo  14391  hashfzp1  14393  hashxplem  14395  hashxp  14396  hashmap  14397  hashpw  14398  hashbclem  14414  hashbc  14415  hashfacen  14416  hashf1lem1  14417  hashf1lem2  14418  hashf1  14419  seqcoll  14426  eqs1  14575  swrdspsleq  14628  pfxeq  14658  pfxsuff1eqwrdeq  14661  ccatopth2  14679  cats1un  14683  swrdccatin1  14687  swrdccat3blem  14701  cshf1  14772  repswcshw  14774  s2eq2s1eq  14898  s3eqs2s1eq  14900  pfx2  14909  2swrd2eqwrdeq  14915  wwlktovf1  14919  eqwrds3  14923  relexpsucnnr  14987  relexpsucnnl  14992  relexpcnv  14997  relexpaddnn  15013  replim  15078  cjreb  15085  cjexp  15112  absexp  15266  abs1m  15298  recan  15299  cnsqrt00  15355  isercoll2  15631  iseraltlem2  15645  iseraltlem3  15646  sumeq2ii  15655  zsum  15680  fsum  15682  fsumf1o  15685  sumss  15686  fsumcvg2  15689  fsumadd  15702  isummulc2  15724  fsum2d  15733  fsummulc2  15746  fsumconst  15752  modfsummods  15756  modfsummod  15757  fsumparts  15769  fsumrelem  15770  fsumiun  15784  binom  15795  bcxmas  15800  incexclem  15801  isumshft  15804  isumnn0nn  15807  climcndslem1  15814  climcndslem2  15815  mertenslem2  15850  clim2prod  15853  prodfrec  15860  prodeq2ii  15876  zprod  15902  fprod  15906  fprodf1o  15911  fprodser  15914  fprodmul  15925  fproddiv  15926  prodsn  15927  prodsnf  15929  fprodabs  15939  fprodconst  15943  fprod2d  15946  fprodmodd  15962  binomfallfac  16006  bpolydif  16020  fprodefsum  16060  efne0d  16062  efne0OLD  16064  efexp  16068  demoivreALT  16168  moddvds  16232  bitsinv1  16411  sadadd2  16429  smu01lem  16454  smupval  16457  smueqlem  16459  smumullem  16461  gcdaddm  16494  bezoutlem1  16508  bezout  16512  gcddiv  16520  seq1st  16540  alginv  16544  algfx  16549  lcmneg  16572  lcmid  16578  lcmgcdeq  16581  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem  16610  lcmfunsn  16613  lcmfun  16614  divgcdcoprm0  16634  cncongr1  16636  cncongr2  16637  nn0gcdsq  16722  crth  16748  eulerthlem2  16752  pythagtriplem1  16787  iserodd  16806  pcqmul  16824  pcexp  16830  pcneg  16845  pcmpt  16863  pcfac  16870  prmreclem2  16888  prmreclem3  16889  1arith  16898  vdwpc  16951  ramcl  17000  prmop1  17009  imasval  17475  ercpbllem  17512  iscat  17638  iscatd  17639  catideu  17641  iscatd2  17647  catlid  17649  catrid  17650  catass  17652  homfeq  17660  comfeq  17672  catpropd  17675  moni  17703  epii  17710  sectffval  17717  sectfval  17718  oppcsect  17745  sectmon  17749  isfunc  17831  funcid  17837  funcco  17838  funcpropd  17869  isfull  17879  fthsect  17894  fthmon  17896  natfval  17916  isnat  17917  nati  17925  fucsect  17942  natpropd  17946  setcmon  18054  setcepi  18055  setcsect  18056  fthestrcsetc  18116  embedsetcestrclem  18123  fthsetcestrc  18131  evlfcl  18188  uncfcurf  18205  yoniso  18251  joinval  18341  meetval  18355  islat  18399  latdisdlem  18462  latdisd  18463  isclat  18466  isdlat  18488  dlatmjdi  18489  isacs5lem  18511  acsdrscl  18512  acsficl  18513  isps  18534  mgmidmo  18628  mgmlrid  18635  lidrideqd  18637  lidrididd  18638  grpinvalem  18641  grpinva  18642  gsumvalx  18644  gsumval2  18654  ismgmhm  18664  mgmhmpropd  18666  mgmhmlin  18667  mgmhmeql  18684  issgrp  18688  isnsgrp  18691  sgrpass  18693  sgrp1  18697  issgrpd  18698  sgrppropd  18699  ismndd  18724  mndpropd  18727  imasmnd2  18742  xpsmnd0  18746  mnd1  18747  mnd1id  18748  ismhm  18753  mhmpropd  18760  mhmlin  18761  mhmimalem  18792  mhmeql  18794  gsumccat  18809  gsumwmhm  18813  frmdgsum  18830  symggrplem  18852  smndex1mndlem  18880  smndex1n0mnd  18883  sgrp2rid2  18897  sgrp2nmndlem4  18899  isgrp  18915  grppropd  18927  isgrpd2e  18931  dfgrp2  18938  isgrpid2  18952  grpidd2  18953  grpinvfval  18954  grpinvfvalALT  18955  grpinv11  18983  grpinvpropd  18991  grpidssd  18992  grpinvssd  18993  grpsubrcan  18997  dfgrp3lem  19014  grplactcnv  19019  imasgrp2  19031  mhmlem  19038  mulgnn0p1  19061  mulgaddcom  19074  mulginvcom  19075  mulgneg2  19084  mulgnnass  19085  mulgnn0ass  19086  mulgass  19087  mhmmulg  19091  cyccom  19178  isghm  19190  isghmOLD  19191  ghmlin  19196  ghmeql  19214  isga  19266  gagrpid  19269  gaass  19272  galcan  19279  orbsta  19288  cntzfval  19295  elcntz  19297  cntzsnval  19299  elcntzsn  19300  cntzi  19304  resscntz  19308  cntzmhm  19316  gsumwrev  19341  snsymgefmndeq  19370  cayleylem2  19388  symgextf1  19396  gsmsymgreqlem2  19406  gsmsymgreq  19407  symgfixf1  19412  pmtrfrn  19433  odfval  19507  odfvalALT  19508  mndodcong  19517  odbezout  19533  odeq1  19535  submod  19544  gexval  19553  gexdvds  19559  ispgp  19567  sylow1lem1  19573  sylow2alem1  19592  sylow2alem2  19593  sylow2blem2  19596  efgmnvl  19689  efgredlemc  19720  efgredeu  19727  frgpuptinv  19746  frgpup1  19750  frgpup3lem  19752  iscmn  19764  cmnpropd  19766  iscmnd  19769  abladdsub4  19786  submcmn2  19814  qusabl  19840  abl1  19841  imasabl  19851  iscyg  19854  cycsubmcmn  19864  gsum2dlem2  19946  telgsumfzs  19964  dmdprd  19975  dprdval  19980  dprdfcntz  19992  subgdmdprd  20011  dprd2da  20019  dpjrid  20039  pgpfac1lem3a  20053  ablfaclem3  20064  ablfac2  20066  gsumle  20120  isrng  20135  rngdi  20141  rngdir  20142  rngpropd  20155  imasrng  20158  ringurd  20166  issrg  20169  o2timesd  20191  rglcom4d  20192  srgmulgass  20198  srgpcomp  20199  srgbinom  20212  isring  20218  ringpropd  20269  ringinvnz1ne0  20281  mulgass2  20290  ring1  20291  imasring  20310  xpsring1d  20313  dvdsr  20342  dvreq1  20391  rnghmval  20420  isrnghm  20421  rnghmmul  20429  c0snmgmhm  20442  rngisomring1  20448  zrrnghm  20513  islring  20517  rngcsect  20613  ringcsect  20647  rrgval  20674  unitrrg  20680  domnlcanb  20697  domnrcanb  20699  isdrng  20710  drngprop  20721  isdrngd  20742  isdrngdOLD  20744  drngpropd  20746  cntzsdrg  20779  isabv  20788  abvmul  20798  issrng  20821  issrngd  20832  idsrngd  20833  islmod  20859  lmodlema  20860  islmodd  20861  lmodvsmmulgdi  20892  lmodprop2d  20919  rmodislmodlem  20924  rmodislmod  20925  islmhm  21022  lmhmlin  21030  islmhm2  21033  lmhmeql  21050  lmhmpropd  21068  islbs  21071  lbspropd  21094  rnglidlmsgrp  21244  rnglidlrng  21245  quscrng  21281  rngqiprngimfo  21299  islpir  21326  cnfldmulg  21384  cnfldexp  21385  prmirredlem  21452  pzriprnglem6  21466  pzriprnglem10  21470  pzriprnglem12  21472  chrcong  21507  zndvds  21529  znf1o  21531  znunit  21543  cygznlem3  21549  frgpcyg  21553  psgndiflemB  21580  isphl  21608  ipcj  21614  iporthcom  21615  ip2eq  21633  isphld  21634  phlpropd  21635  phlssphl  21639  ocvfval  21646  iscss  21663  ishil  21698  isobs  21700  obsip  21701  obslbs  21710  frlmphl  21761  isassa  21836  assalem  21837  isassad  21845  assapropd  21851  assamulgscm  21881  mvrf1  21964  mplmonmul  22014  mplcoe1  22015  mplcoe3  22016  mplcoe5lem  22017  mplcoe5  22018  evlslem1  22060  mpfrcl  22063  evlsval  22064  psdpw  22136  coe1tm  22238  ply1sclf1  22254  ply1coe  22263  eqcoe1ply1eq  22264  cply1coe0bi  22267  coe1fzgsumd  22269  ply1scleq  22270  ply1chr  22271  gsumply1eq  22274  evl1gsumd  22322  mat0dimcrng  22435  mat1ghm  22448  mat1mhm  22449  dmatcrng  22467  scmateALT  22477  scmatcrng  22486  scmatf1  22496  mvmumamul1  22519  mdetdiagid  22565  mdetralt  22573  mdetunilem1  22577  mdetunilem3  22579  mdetunilem4  22580  mdetunilem7  22583  mdetunilem9  22585  mdetuni0  22586  madugsum  22608  smadiadetr  22640  mat2pmatf1  22694  m2cpminvid2lem  22719  decpmataa0  22733  pmatcollpw2lem  22742  pm2mpf1  22764  chcoeffeqlem  22850  chcoeffeq  22851  cayhamlem3  22852  cayleyhamilton1  22857  isperf  23116  restperf  23149  cmpsub  23365  isconn  23378  2ndcsep  23424  elptr2  23539  ptbasin  23542  dfac14  23583  txcnp  23585  ptcnplem  23586  ptcnp  23587  cnmpt11  23628  cnmpt21  23636  cnmptcom  23643  kqfeq  23689  isr0  23702  pt1hmeo  23771  ustexsym  24181  isusp  24226  imasdsf1olem  24338  isxms  24412  xmspropd  24438  imasf1oxms  24454  stdbdmopn  24483  isngp3  24563  ngppropd  24602  tngngp3  24621  isnlm  24640  nmvs  24641  xrsxmet  24775  cnheibor  24922  htpyi  24941  htpycc  24947  pi1xfr  25022  pi1coghm  25028  isclm  25031  lmhmclm  25054  isclmp  25064  clmmulg  25068  iscph  25137  tcphcph  25204  cphsscph  25218  cmetcaulem  25255  bcth3  25298  ovolunlem1a  25463  ovolicc2lem1  25484  ovolicc2lem4  25487  ovolicc2  25489  mblsplit  25499  volun  25512  volfiniun  25514  voliunlem1  25517  volsup  25523  ioorinv  25543  uniioombllem2  25550  vitalilem3  25577  mbfeqalem1  25608  mbflim  25635  itgeqa  25781  itgconst  25786  itgfsum  25794  itgsplitioo  25805  dvnadd  25896  dvnres  25898  dvexp  25920  dvmptfsum  25942  mvth  25959  dvlip  25960  lhop1lem  25980  dvcvx  25987  mdegle0  26042  ply1nzb  26088  mon1pval  26107  facth1  26132  ig1pval  26141  dgrmulc  26236  dgrcolem1  26238  dgrcolem2  26239  dgrco  26240  coecj  26243  coecjOLD  26245  vieta1lem2  26277  vieta1  26278  elqaalem3  26287  dvntaylp  26336  ulmss  26362  mtest  26369  sineq0  26488  efif1olem4  26509  cxpexp  26632  mulcxplem  26648  mulcxp  26649  cxpmul2  26653  cxpeq  26721  affineequiv2  26788  quad2  26803  dcubic  26810  leibpi  26906  o1cxp  26938  scvxcvx  26949  facgam  27029  wilthlem1  27031  wilthlem2  27032  mpodvdsmulf1o  27157  fsumdvdsmul  27158  perfect  27194  dchrelbas2  27200  dchrinv  27224  dchrptlem2  27228  lgsne0  27298  lgsqrlem2  27310  lgsdchr  27318  gausslemma2d  27337  lgseisenlem2  27339  lgsquad2lem2  27348  2lgslem1a  27354  2lgslem1b  27355  dchrisumlem1  27452  qabvexp  27589  ostthlem1  27590  ostthlem2  27591  ostth3  27601  ltsval2  27620  ltsres  27626  nolesgn2ores  27636  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  noinfcbv  27681  noinfno  27682  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  addsrid  27956  addscom  27958  addscan1  27986  addsass  27997  subscan1d  28095  subscan2d  28096  mulsrid  28105  mulscom  28131  addsdilem3  28145  addsdilem4  28146  addsdi  28147  mulsasslem3  28157  mulsass  28158  mulscan2d  28171  mulscan1d  28172  bdayons  28268  om2noseqrdg  28296  n0cut  28326  expadds  28427  pw2cut  28452  pw2cut2  28454  elreno  28483  istrkgc  28522  istrkgcb  28524  istrkgld  28527  istrkg2ld  28528  axtgcgrrflx  28530  axtgupdim2  28539  tgjustf  28541  tgjustr  28542  iscgrg  28580  iscgrglt  28582  trgcgrg  28583  tgcgr4  28599  motcgr  28604  legso  28667  mirval  28723  israg  28765  ismidb  28846  isinagd  28907  f1otrgds  28937  ttgval  28943  ttgitvval  28950  brcgr  28969  brbtwn2  28974  colinearalglem1  28975  colinearalg  28979  ax5seglem1  28997  ax5seglem2  28998  ax5seglem8  29005  ax5seglem9  29006  axlowdimlem13  29023  axlowdimlem16  29026  axlowdim1  29028  axcontlem1  29033  axcontlem2  29034  axcontlem6  29038  axcontlem7  29039  axcontlem8  29040  ecgrtg  29052  usgredg2v  29296  issubgr  29340  cplgruvtxb  29482  cusgrsize  29523  finsumvtxdg2size  29619  isrgr  29628  wkslem1  29676  wkslem2  29677  iswlk  29679  uspgr2wlkeq  29714  2wlklem  29734  wlkres  29737  redwlk  29739  wlkp1lem6  29745  wlkp1lem7  29746  wlkp1lem8  29747  pthdivtx  29795  upgrwlkdvdelem  29804  isclwlk  29841  iscrct  29858  iscycl  29859  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  wwlksnextinj  29967  rusgrnumwwlk  30046  clwlkclwwlklem2  30070  clwlkclwwlkf1lem3  30076  clwlkclwwlkf1  30080  erclwwlkeq  30088  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  erclwwlkneq  30137  clwwlkvbij  30183  upgreupthseg  30279  eupth2eucrct  30287  eupth2lem3  30306  eupth2  30309  eucrctshift  30313  2clwwlk  30417  numclwwlk1lem2f1  30427  numclwlk1lem1  30439  numclwlk1lem2  30440  numclwlk2lem2f1o  30449  isgrpo  30568  grpoass  30574  grpoidinvlem3  30577  grpoidinv  30579  grpoideu  30580  grpoidinv2  30586  grpoinvfval  30593  isablo  30617  ablocom  30619  vciOLD  30632  vcidOLD  30635  vcdi  30636  vcdir  30637  vcass  30638  isvclem  30648  isnvlem  30681  nvmeq0  30729  nvs  30734  imsmetlem  30761  islno  30824  lnolin  30825  ishmo  30882  isphg  30888  phpar2  30894  phpar  30895  ipdiri  30901  ipasslem1  30902  ipasslem5  30906  ipasslem11  30911  ipassi  30912  dipdir  30913  dipass  30916  ip2eqi  30927  htth  30989  hvsubsub4  31131  hvnegdi  31138  hvaddcan  31141  hvaddcan2  31142  hvsubcan  31145  hvsubcan2  31146  hvaddsub4  31149  hial2eq  31177  normlem9at  31192  normsq  31205  norm-iii  31211  normsub  31214  normpyth  31216  normpar  31226  polid  31230  issubgoilem  31331  ococ  31477  chj0  31568  chlejb1  31583  chdmm1  31596  chjass  31604  spanun  31616  spansn  31630  elspansn2  31638  cmbr  31655  cmbr3  31679  pjoml2  31682  pjoml3  31683  osum  31716  spansnj  31718  pjch1  31741  pjadji  31756  pjaddi  31757  pjinormi  31758  pjsubi  31759  pjmuli  31760  pjcjt2  31763  pjch  31765  pjopyth  31791  pjpyth  31796  hoaddcom  31845  hoaddass  31853  hocsubdir  31856  hoaddrid  31862  ho0sub  31868  honegsub  31870  adjsym  31904  eigrei  31905  eigre  31906  eigposi  31907  eigorth  31909  ellnop  31929  elhmop  31944  ellnfn  31954  cnvadj  31963  lnopl  31985  unop  31986  hmop  31993  lnfnl  32002  adj1  32004  eleigvec  32028  hoddi  32061  lnopeq0lem2  32077  lnopunilem1  32081  lnopunilem2  32082  lnopunii  32083  elunop2  32084  lnophmi  32089  lnfnmul  32119  cnlnadjlem5  32142  branmfn  32176  bra11  32179  hmopidmchi  32222  hmopidmch  32224  hmopidmpj  32225  pjss2coi  32235  pjssmi  32236  pjssge0i  32237  pjidmco  32252  dfpjop  32253  elpjrn  32261  isst  32284  ishst  32285  hstel2  32290  stj  32306  mdbr  32365  mdi  32366  mdbr3  32368  dmdbr  32370  dmdmd  32371  dmdi  32373  dmdbr3  32376  mddmd2  32380  mdsl1i  32392  chjatom  32428  iuninc  32630  fmptcof2  32730  receqid  32817  bcm1n  32868  fsumiunle  32902  sgnsgn  32914  xmulcand  32980  xrsmulgzz  33069  psgnfzto1st  33166  isfxp  33229  fxpgaeq  33230  isslmd  33263  slmdlema  33264  gsumvsca1  33287  gsumvsca2  33288  urpropd  33292  elrgspnsubrunlem2  33309  erlval  33319  domnpropd  33338  domnlcanOLD  33341  qusvscpbl  33411  nsgqusf1olem3  33475  opprqusdrng  33553  ressply1mon1p  33628  ressply1invg  33629  deg1prod  33643  ply1moneq  33648  psrgsum  33692  psrmonmul  33694  psrmonprod  33696  vietalem  33723  vieta  33724  fedgmul  33775  brfldext  33789  fldextrspunlsplem  33817  extdgfialglem1  33836  bralgext  33841  minplyval  33849  submateq  33953  dispcmp  34003  pstmxmet  34041  cnre2csqlem  34054  mndpluscn  34070  qqhval2  34126  isrrext  34144  esumfzf  34213  esumcvg  34230  esum2dlem  34236  esumiun  34238  ofcfeqd2  34245  ismeas  34343  isrnmeas  34344  measvun  34353  carsgval  34447  inelcarsg  34455  carsgclctunlem1  34461  carsgclctunlem2  34463  pmeasmono  34468  pmeasadd  34469  eulerpartlemgvv  34520  eulerpartlemn  34525  sseqp1  34539  probun  34563  breprexp  34777  istrkg2d  34810  axtgupdim2ALTV  34812  afsval  34815  bnj1385  34974  bnj66  35002  bnj106  35010  bnj155  35021  bnj222  35025  bnj540  35034  bnj591  35053  bnj594  35054  bnj611  35060  bnj893  35070  bnj1000  35083  bnj966  35086  bnj1112  35125  bnj1234  35155  bnj1253  35159  bnj1280  35162  bnj1326  35168  bnj1450  35192  bnj1463  35197  bnj1529  35212  f1resveqaeq  35228  pfxwlk  35306  revwlk  35307  subfacp1lem3  35364  subfacp1lem4  35365  subfacp1lem5  35366  subfacp1lem6  35367  subfacval2  35369  erdszelem9  35381  sconnpht  35411  ptpconn  35415  cvmliftmolem1  35463  cvmliftmolem2  35464  cvmliftlem10  35476  cvmlift2  35498  cvmliftphtlem  35499  satfdm  35551  gonarlem  35576  gonar  35577  goalr  35579  satfdmfmla  35582  prv  35610  mrsubff1  35696  mrsubccat  35700  elmrsubrn  35702  mrsubvrs  35704  elmpst  35718  msrid  35727  msubvrs  35742  sqdivzi  35910  shftvalg  35914  bcprod  35920  bccolsum  35921  iprodefisumlem  35922  faclimlem1  35925  rdgprc  35974  dfrdg2  35975  elwlim  36003  fvsingle  36100  fullfunfv  36129  lineelsb2  36330  rankung  36348  ranksng  36349  rankpwg  36351  opnregcld  36512  cldregopn  36513  neibastop3  36544  weiunval  36644  csbttc  36691  mh-inf3f1  36723  bj-sbeqALT  37207  bj-gabeqis  37245  bj-isclm  37605  rdgeqoa  37686  fvineqsnf1  37726  tan2h  37933  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem9  37950  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem19  37960  broucube  37975  voliunnfl  37985  volsupnfl  37986  cocanfo  38040  upixp  38050  sdclem2  38063  caushft  38082  ismtycnv  38123  ismtyima  38124  ismtybndlem  38127  ismtyres  38129  bfplem2  38144  bfp  38145  isass  38167  opidonOLD  38173  exidu1  38177  cmpidelt  38180  grpoeqdivid  38202  elghomlem2OLD  38207  ghomlinOLD  38209  ghomco  38212  isrngo  38218  rngoid  38223  rngoideu  38224  rngodi  38225  rngodir  38226  rngoass  38227  rngohomval  38285  isrngohom  38286  rngohomadd  38290  rngohommul  38291  iscom2  38316  iscringd  38319  crngocom  38322  crngohomfo  38327  dmncan2  38398  elsymrels4  38960  brredunds  39031  lshpset  39424  lcvexchlem4  39483  lcvexchlem5  39484  lflset  39505  islfl  39506  lfli  39507  islfld  39508  eqlkr3  39547  isopos  39626  oposlem  39628  opcon3b  39642  cmtvalN  39657  omllaw  39689  cvlexchb2  39777  cvlatexchb2  39781  cvlsupr2  39789  4atlem9  40049  4atlem10a  40050  4atlem11a  40053  4atlem12a  40056  4at2  40060  pmapglb2N  40217  pmapglb2xN  40218  paddasslem17  40282  ispsubclN  40383  ispsubcl2N  40393  lhpmod2i2  40484  lhpmod6i1  40485  4atexlemex2  40517  4atex  40522  4atex2-0aOLDN  40524  4atex2-0cOLDN  40526  ldilval  40559  ltrnfset  40563  ltrnset  40564  isltrn  40565  ltrneq2  40594  trnfsetN  40601  trnsetN  40602  istrnN  40603  cdlemd5  40648  cdleme0moN  40671  cdleme0nex  40736  cdleme18d  40741  cdleme31so  40825  cdleme31fv  40836  cdlemg2jlemOLDN  41039  cdlemg2fvlem  41040  cdlemg2klem  41041  istendo  41206  tendovalco  41211  tendoeq2  41220  dicelvalN  41624  dihval  41678  dihcnv11  41721  dihmeetlem13N  41765  dihlspsnat  41779  dochn0nv  41821  dochkrshp4  41835  lpolsetN  41928  lpolsatN  41934  lpolpolsatN  41935  lcfl1lem  41937  lclkrlem2a  41953  lclkrlem2e  41957  lcfls1lem  41980  lclkrs2  41986  lcdfval  42034  lcdval  42035  mapdffval  42072  mapdfval  42073  mapd0  42111  mapdpglem30  42148  mapdhval  42170  mapdheq2  42175  hdmap1vallem  42243  hdmap1val  42244  hdmap1cbv  42248  hdmapval3N  42284  hdmap10  42286  hdmapeq0  42290  hdmap14lem12  42325  hdmap14lem13  42326  hgmapfval  42332  hgmapvs  42337  hgmapvv  42372  hlhilocv  42403  recbothd  42431  lcmineqlem13  42480  isprimroot  42532  primrootsunit1  42536  aks6d1c1p1  42546  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  evl1gprodd  42556  aks6d1c1rh  42564  aks6d1c2lem3  42565  deg1gprod  42579  deg1pow  42580  sticksstones22  42607  aks6d1c6lem2  42610  aks5lem3a  42628  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  ccatcan2d  42690  remulcan2d  42695  sumcubes  42745  expeqidd  42757  cxp112d  42773  cxp111d  42774  log11d  42778  sn-addcand  42852  sn-addcan2d  42854  sn-mullid  42868  nn0addcom  42907  renegmulnnass  42910  nn0mulcom  42911  zmulcomlem  42912  cnreeu  42935  abvexp  42977  fiabv  42981  prjsprel  43037  prjcrvfval  43064  flt0  43070  sn-isghm  43106  ismrcd2  43131  ismrc  43133  dvdsrabdioph  43238  fphpdo  43245  rmxypairf1o  43339  monotoddzzfi  43370  monotoddzz  43371  oddcomabszz  43372  rmxdioph  43444  expdiophlem2  43450  dnnumch3  43475  aomclem8  43489  islssfg  43498  unxpwdom3  43523  gicabl  43527  idomodle  43619  fgraphxp  43632  hausgraph  43633  onov0suclim  43702  oaabsb  43722  oaomoencom  43745  oenass  43747  omabs2  43760  tfsconcat0b  43774  nadd1suc  43820  naddonnn  43823  minregex  43961  relexpmulnn  44136  clsk1independent  44473  ntrclsk13  44498  ntrclsk4  44499  imo72b2  44599  grumnud  44713  nzss  44744  caofcan  44750  expgrowth  44762  fsneq  45635  fperiodmullem  45736  uzinico3  45992  fsumf1of  46004  fmuldfeq  46013  fprodexp  46024  fprodabs2  46025  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climaddf  46045  mullimc  46046  limcperiod  46058  neglimc  46075  addlimc  46076  0ellimcdiv  46077  climeldmeqmpt  46096  climfveqmpt  46099  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  climeqf  46116  climeldmeqmpt3  46117  limsupequz  46151  cncfperiod  46307  icccncfext  46315  fperdvper  46347  dvnmptdivc  46366  dvnxpaek  46370  dvnmul  46371  dvmptfprod  46373  dvnprodlem3  46376  itgspltprt  46407  stoweidlem30  46458  stoweidlem48  46476  wallispilem4  46496  wallispi2lem1  46499  wallispi2lem2  46500  fourierdlem50  46584  fourierdlem73  46607  fourierdlem81  46615  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem94  46628  fourierdlem97  46631  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  sge0iunmptlemfi  46841  ismea  46879  meadjuni  46885  meaiuninclem  46908  caragenval  46921  isome  46922  caragensplit  46928  carageniuncllem1  46949  caratheodorylem1  46954  hoidmvlelem3  47025  vonvolmbllem  47088  vonvolmbl  47089  smflimlem3  47201  smflim  47205  smfpimcc  47236  smfsuplem2  47240  fsetsnf1  47500  cfsetsnfsetf1  47507  fcoresf1  47517  csbafv12g  47585  csbaovg  47628  csbafv212g  47667  mod2addne  47818  fargshiftf1  47901  fargshiftfva  47903  prproropf1olem4  47966  fmtnorec2  48006  fmtnoprmfac1lem  48027  fmtnofac1  48033  quad1  48096  requad1  48098  perfectALTV  48199  fpprwppr  48215  nfermltl8rev  48218  nfermltl2rev  48219  nfermltlrev  48220  sbgoldbo  48263  isgrim  48358  grimuhgr  48363  grimcnv  48364  grimco  48365  uhgrimedgi  48366  isuspgrim0  48370  upgrimwlklem5  48377  gricushgr  48393  isubgrgrim  48405  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  uspgrlimlem3  48466  uspgrlimlem4  48467  grlimedgclnbgr  48471  grlimgrtrilem2  48478  gpgvtxedg0  48539  gpgvtxedg1  48540  uspgrsprf1  48623  plusfreseq  48640  iscomlaw  48666  isasslaw  48668  lidldomn1  48707  zlidlring  48710  rngcsectALTV  48751  ringcsectALTV  48785  ovmpordxf  48815  lmodvsmdi  48855  islininds  48922  lindslinindimp2lem4  48937  lindslinindsimp2  48939  lmod1  48968  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  nn0sumshdig  49099  1arymaptf1  49118  2arymaptf1  49129  itcovalpc  49148  itcovalt2  49153  rrx2pnecoorneor  49191  rrx2plordisom  49199  rrx2line  49216  rrx2linest  49218  line2ylem  49227  line2x  49230  line2y  49231  itscnhlc0yqe  49235  itscnhlc0xyqsol  49241  idmon  49495  idepi  49496  sectpropdlem  49511  ssccatid  49547  imaidfu  49585  oppff1  49623  imasubc  49626  diag1f1lem  49781  diag2f1lem  49783  fucofvalne  49800  catcsect  49873  grptcmon  50068  grptcepi  50069  aacllem  50276