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 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 2709

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

This theorem is referenced by:  neeq12d  2994  cdeqeq  3722  sbceqg  4353  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  iununi  5042  csbopab  5504  csbopabgALT  5505  dfid2  5522  csbima12  6039  dmsnsnsn  6179  csbcog  6256  dfpred3g  6272  preddowncl  6291  limeq  6330  csbiota  6486  fveqres  6879  opabiota  6917  fvmptf  6964  eqfnfv2f  6982  fvreseq0  6985  fveqdmss  7025  fvcofneq  7040  fnressn  7106  fnelfp  7124  fprb  7143  fnprb  7157  fntpb  7158  f1cofveqaeqALT  7207  nvocnv  7230  cocan1  7240  cocan2  7241  2fvcoidd  7246  fliftfun  7261  weniso  7303  csbriota  7333  oveqrspc2v  7388  csbov123  7405  eqfnov  7490  ovmpos  7509  ov2gf  7510  ovmpodxf  7511  caovcomg  7556  caovassg  7559  caovcang  7562  caovcanrd  7564  caovcan  7565  caovdig  7575  caovdirg  7578  caovmo  7598  coof  7649  offveqb  7652  caofid0l  7658  caofid0r  7659  caofidlcan  7663  caofass  7665  caonncan  7669  ordunisuc  7777  onsucuni2  7779  orduninsuc  7788  op1stg  7948  op2ndg  7949  f1o2ndf1  8066  xpord2pred  8089  xpord3pred  8096  poseq  8102  soseq  8103  fnsuppres  8135  csbfrecsg  8228  fpr3g  8229  frrlem1  8230  frrlem12  8241  frrlem13  8242  fpr2a  8246  wfr3g  8263  onfununi  8275  tfrlem1  8309  tfrlem3a  8310  tfrlem5  8313  tfrlem9  8318  tfrlem11  8321  tfrlem12  8322  tfr3  8332  tz7.44-1  8339  tz7.44-2  8340  tz7.44-3  8341  rdglem1  8348  rdg0g  8360  seqomlem1  8383  oalim  8461  omlim  8462  oelim  8463  oa0r  8467  om0r  8468  om1r  8472  oaass  8490  oarec  8491  odi  8508  omass  8509  oelim2  8525  oeoalem  8526  oeoa  8527  oeoelem  8528  oeoe  8529  nna0r  8539  nnacom  8547  nnaass  8552  nndi  8553  nnmass  8554  nnmsucr  8555  nnmcom  8556  oaabs  8578  oaabs2  8579  omabs  8581  naddcllem  8606  naddcom  8612  naddrid  8613  naddass  8626  naddsuc2  8631  naddoa  8632  ecovcom  8764  ecovass  8765  ecovdi  8766  dom2lem  8933  unxpdomlem2  9161  unxpdomlem3  9162  ixpfi2  9254  fipreima  9262  ordiso2  9424  wemaplem1  9455  wemaplem2  9456  wemapsolem  9459  cantnfval2  9584  cantnfp1lem3  9595  oemapvali  9599  cantnflem1c  9602  cantnflem1  9604  wemapwe  9612  rnttrcl  9637  tcvalg  9651  frr3g  9674  frr2  9678  rankvalg  9735  rankonidlem  9746  ranklim  9762  rankuni  9781  updjud  9852  cardprclem  9897  cardprc  9898  carduni  9899  fseqenlem1  9940  fodomacn  9972  alephcard  9986  alephfp2  10025  alephval3  10026  dfac12lem1  10060  dfac12lem2  10061  dfac12r  10063  ackbij1lem8  10142  ackbij1lem14  10148  ackbij1lem16  10150  ackbij2lem3  10156  cardcf  10168  sornom  10193  fin23lem28  10256  isf32lem2  10270  itunitc  10337  ituniiun  10338  axdc3lem2  10367  axdc4lem  10371  ttukeylem3  10427  ttukey2g  10432  fpwwe2lem7  10554  fpwwecbv  10561  canth4  10564  pwfseqlem2  10576  addcanpi  10816  mulcanpi  10817  recrecnq  10884  ltexnq  10892  genpv  10916  0idsr  11014  1idsr  11015  ax1rid  11078  mulrid  11136  addcan  11324  addcan2  11325  mulcand  11777  mulcan2d  11778  mulcan2g  11798  div11OLD  11832  divmuleq  11854  conjmul  11866  eqneg  11869  ofsubeq0  12150  nnadd1com  12194  nnaddcom  12195  nnadddir  12227  nnmul1com  12228  nnmulcom  12229  rpnnen1lem6  12926  cnref1o  12929  xmulasslem  13231  xmulass  13233  xadddi2  13243  prunioo  13428  fzsuc2  13530  fzprval  13533  fztpval  13534  fzosplitprm1  13727  modadd1  13861  modaddb  13862  modmul1  13880  addmodlteq  13902  om2uzsuci  13904  om2uzrdg  13912  uzrdgxfr  13923  seq1  13970  seqp1  13972  seqfveq2  13980  seqfveq  13982  seqshft2  13984  seqsplit  13991  seqcaopr3  13993  seqcaopr2  13994  seqf1olem2a  13996  seqf1olem2  13998  seqf1o  13999  seqid  14003  seqid2  14004  seqhomo  14005  ser1const  14014  seqof2  14016  mulexp  14057  expadd  14060  expmul  14063  binom2  14173  sq01  14181  modexp  14194  bcpasc  14277  hashgadd  14333  hashdom  14335  hashfzo  14385  hashfzp1  14387  hashxplem  14389  hashxp  14390  hashmap  14391  hashpw  14392  hashbclem  14408  hashbc  14409  hashfacen  14410  hashf1lem1  14411  hashf1lem2  14412  hashf1  14413  seqcoll  14420  eqs1  14569  swrdspsleq  14622  pfxeq  14652  pfxsuff1eqwrdeq  14655  ccatopth2  14673  cats1un  14677  swrdccatin1  14681  swrdccat3blem  14695  cshf1  14766  repswcshw  14768  s2eq2s1eq  14892  s3eqs2s1eq  14894  pfx2  14903  2swrd2eqwrdeq  14909  wwlktovf1  14913  eqwrds3  14917  relexpsucnnr  14981  relexpsucnnl  14986  relexpcnv  14991  relexpaddnn  15007  replim  15072  cjreb  15079  cjexp  15106  absexp  15260  abs1m  15292  recan  15293  cnsqrt00  15349  isercoll2  15625  iseraltlem2  15639  iseraltlem3  15640  sumeq2ii  15649  zsum  15674  fsum  15676  fsumf1o  15679  sumss  15680  fsumcvg2  15683  fsumadd  15696  isummulc2  15718  fsum2d  15727  fsummulc2  15740  fsumconst  15746  modfsummods  15750  modfsummod  15751  fsumparts  15763  fsumrelem  15764  fsumiun  15778  binom  15789  bcxmas  15794  incexclem  15795  isumshft  15798  isumnn0nn  15801  climcndslem1  15808  climcndslem2  15809  mertenslem2  15844  clim2prod  15847  prodfrec  15854  prodeq2ii  15870  zprod  15896  fprod  15900  fprodf1o  15905  fprodser  15908  fprodmul  15919  fproddiv  15920  prodsn  15921  prodsnf  15923  fprodabs  15933  fprodconst  15937  fprod2d  15940  fprodmodd  15956  binomfallfac  16000  bpolydif  16014  fprodefsum  16054  efne0d  16056  efne0OLD  16058  efexp  16062  demoivreALT  16162  moddvds  16226  bitsinv1  16405  sadadd2  16423  smu01lem  16448  smupval  16451  smueqlem  16453  smumullem  16455  gcdaddm  16488  bezoutlem1  16502  bezout  16506  gcddiv  16514  seq1st  16534  alginv  16538  algfx  16543  lcmneg  16566  lcmid  16572  lcmgcdeq  16575  lcmfunsnlem1  16600  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  lcmfunsnlem  16604  lcmfunsn  16607  lcmfun  16608  divgcdcoprm0  16628  cncongr1  16630  cncongr2  16631  nn0gcdsq  16716  crth  16742  eulerthlem2  16746  pythagtriplem1  16781  iserodd  16800  pcqmul  16818  pcexp  16824  pcneg  16839  pcmpt  16857  pcfac  16864  prmreclem2  16882  prmreclem3  16883  1arith  16892  vdwpc  16945  ramcl  16994  prmop1  17003  imasval  17469  ercpbllem  17506  iscat  17632  iscatd  17633  catideu  17635  iscatd2  17641  catlid  17643  catrid  17644  catass  17646  homfeq  17654  comfeq  17666  catpropd  17669  moni  17697  epii  17704  sectffval  17711  sectfval  17712  oppcsect  17739  sectmon  17743  isfunc  17825  funcid  17831  funcco  17832  funcpropd  17863  isfull  17873  fthsect  17888  fthmon  17890  natfval  17910  isnat  17911  nati  17919  fucsect  17936  natpropd  17940  setcmon  18048  setcepi  18049  setcsect  18050  fthestrcsetc  18110  embedsetcestrclem  18117  fthsetcestrc  18125  evlfcl  18182  uncfcurf  18199  yoniso  18245  joinval  18335  meetval  18349  islat  18393  latdisdlem  18456  latdisd  18457  isclat  18460  isdlat  18482  dlatmjdi  18483  isacs5lem  18505  acsdrscl  18506  acsficl  18507  isps  18528  mgmidmo  18622  mgmlrid  18629  lidrideqd  18631  lidrididd  18632  grpinvalem  18635  grpinva  18636  gsumvalx  18638  gsumval2  18648  ismgmhm  18658  mgmhmpropd  18660  mgmhmlin  18661  mgmhmeql  18678  issgrp  18682  isnsgrp  18685  sgrpass  18687  sgrp1  18691  issgrpd  18692  sgrppropd  18693  ismndd  18718  mndpropd  18721  imasmnd2  18736  xpsmnd0  18740  mnd1  18741  mnd1id  18742  ismhm  18747  mhmpropd  18754  mhmlin  18755  mhmimalem  18786  mhmeql  18788  gsumccat  18803  gsumwmhm  18807  frmdgsum  18824  symggrplem  18846  smndex1mndlem  18874  smndex1n0mnd  18877  sgrp2rid2  18891  sgrp2nmndlem4  18893  isgrp  18909  grppropd  18921  isgrpd2e  18925  dfgrp2  18932  isgrpid2  18946  grpidd2  18947  grpinvfval  18948  grpinvfvalALT  18949  grpinv11  18977  grpinvpropd  18985  grpidssd  18986  grpinvssd  18987  grpsubrcan  18991  dfgrp3lem  19008  grplactcnv  19013  imasgrp2  19025  mhmlem  19032  mulgnn0p1  19055  mulgaddcom  19068  mulginvcom  19069  mulgneg2  19078  mulgnnass  19079  mulgnn0ass  19080  mulgass  19081  mhmmulg  19085  cyccom  19172  isghm  19184  isghmOLD  19185  ghmlin  19190  ghmeql  19208  isga  19260  gagrpid  19263  gaass  19266  galcan  19273  orbsta  19282  cntzfval  19289  elcntz  19291  cntzsnval  19293  elcntzsn  19294  cntzi  19298  resscntz  19302  cntzmhm  19310  gsumwrev  19335  snsymgefmndeq  19364  cayleylem2  19382  symgextf1  19390  gsmsymgreqlem2  19400  gsmsymgreq  19401  symgfixf1  19406  pmtrfrn  19427  odfval  19501  odfvalALT  19502  mndodcong  19511  odbezout  19527  odeq1  19529  submod  19538  gexval  19547  gexdvds  19553  ispgp  19561  sylow1lem1  19567  sylow2alem1  19586  sylow2alem2  19587  sylow2blem2  19590  efgmnvl  19683  efgredlemc  19714  efgredeu  19721  frgpuptinv  19740  frgpup1  19744  frgpup3lem  19746  iscmn  19758  cmnpropd  19760  iscmnd  19763  abladdsub4  19780  submcmn2  19808  qusabl  19834  abl1  19835  imasabl  19845  iscyg  19848  cycsubmcmn  19858  gsum2dlem2  19940  telgsumfzs  19958  dmdprd  19969  dprdval  19974  dprdfcntz  19986  subgdmdprd  20005  dprd2da  20013  dpjrid  20033  pgpfac1lem3a  20047  ablfaclem3  20058  ablfac2  20060  gsumle  20114  isrng  20129  rngdi  20135  rngdir  20136  rngpropd  20149  imasrng  20152  ringurd  20160  issrg  20163  o2timesd  20185  rglcom4d  20186  srgmulgass  20192  srgpcomp  20193  srgbinom  20206  isring  20212  ringpropd  20263  ringinvnz1ne0  20275  mulgass2  20284  ring1  20285  imasring  20304  xpsring1d  20307  dvdsr  20336  dvreq1  20385  rnghmval  20414  isrnghm  20415  rnghmmul  20423  c0snmgmhm  20436  rngisomring1  20442  zrrnghm  20507  islring  20511  rngcsect  20607  ringcsect  20641  rrgval  20668  unitrrg  20674  domnlcanb  20691  domnrcanb  20693  isdrng  20704  drngprop  20715  isdrngd  20736  isdrngdOLD  20738  drngpropd  20740  cntzsdrg  20773  isabv  20782  abvmul  20792  issrng  20815  issrngd  20826  idsrngd  20827  islmod  20853  lmodlema  20854  islmodd  20855  lmodvsmmulgdi  20886  lmodprop2d  20913  rmodislmodlem  20918  rmodislmod  20919  islmhm  21017  lmhmlin  21025  islmhm2  21028  lmhmeql  21045  lmhmpropd  21063  islbs  21066  lbspropd  21089  rnglidlmsgrp  21239  rnglidlrng  21240  quscrng  21276  rngqiprngimfo  21294  islpir  21321  cnfldmulg  21396  cnfldexp  21397  prmirredlem  21465  pzriprnglem6  21479  pzriprnglem10  21483  pzriprnglem12  21485  chrcong  21520  zndvds  21542  znf1o  21544  znunit  21556  cygznlem3  21562  frgpcyg  21566  psgndiflemB  21593  isphl  21621  ipcj  21627  iporthcom  21628  ip2eq  21646  isphld  21647  phlpropd  21648  phlssphl  21652  ocvfval  21659  iscss  21676  ishil  21711  isobs  21713  obsip  21714  obslbs  21723  frlmphl  21774  isassa  21849  assalem  21850  isassad  21858  assapropd  21864  assamulgscm  21894  mvrf1  21977  mplmonmul  22027  mplcoe1  22028  mplcoe3  22029  mplcoe5lem  22030  mplcoe5  22031  evlslem1  22073  mpfrcl  22076  evlsval  22077  psdpw  22149  coe1tm  22251  ply1sclf1  22267  ply1coe  22276  eqcoe1ply1eq  22277  cply1coe0bi  22280  coe1fzgsumd  22282  ply1scleq  22283  ply1chr  22284  gsumply1eq  22287  evl1gsumd  22335  mat0dimcrng  22448  mat1ghm  22461  mat1mhm  22462  dmatcrng  22480  scmateALT  22490  scmatcrng  22499  scmatf1  22509  mvmumamul1  22532  mdetdiagid  22578  mdetralt  22586  mdetunilem1  22590  mdetunilem3  22592  mdetunilem4  22593  mdetunilem7  22596  mdetunilem9  22598  mdetuni0  22599  madugsum  22621  smadiadetr  22653  mat2pmatf1  22707  m2cpminvid2lem  22732  decpmataa0  22746  pmatcollpw2lem  22755  pm2mpf1  22777  chcoeffeqlem  22863  chcoeffeq  22864  cayhamlem3  22865  cayleyhamilton1  22870  isperf  23129  restperf  23162  cmpsub  23378  isconn  23391  2ndcsep  23437  elptr2  23552  ptbasin  23555  dfac14  23596  txcnp  23598  ptcnplem  23599  ptcnp  23600  cnmpt11  23641  cnmpt21  23649  cnmptcom  23656  kqfeq  23702  isr0  23715  pt1hmeo  23784  ustexsym  24194  isusp  24239  imasdsf1olem  24351  isxms  24425  xmspropd  24451  imasf1oxms  24467  stdbdmopn  24496  isngp3  24576  ngppropd  24615  tngngp3  24634  isnlm  24653  nmvs  24654  xrsxmet  24788  cnheibor  24935  htpyi  24954  htpycc  24960  pi1xfr  25035  pi1coghm  25041  isclm  25044  lmhmclm  25067  isclmp  25077  clmmulg  25081  iscph  25150  tcphcph  25217  cphsscph  25231  cmetcaulem  25268  bcth3  25311  ovolunlem1a  25476  ovolicc2lem1  25497  ovolicc2lem4  25500  ovolicc2  25502  mblsplit  25512  volun  25525  volfiniun  25527  voliunlem1  25530  volsup  25536  ioorinv  25556  uniioombllem2  25563  vitalilem3  25590  mbfeqalem1  25621  mbflim  25648  itgeqa  25794  itgconst  25799  itgfsum  25807  itgsplitioo  25818  dvnadd  25909  dvnres  25911  dvexp  25933  dvmptfsum  25955  mvth  25972  dvlip  25973  lhop1lem  25993  dvcvx  26000  mdegle0  26055  ply1nzb  26101  mon1pval  26120  facth1  26145  ig1pval  26154  dgrmulc  26249  dgrcolem1  26251  dgrcolem2  26252  dgrco  26253  coecj  26256  coecjOLD  26258  vieta1lem2  26291  vieta1  26292  elqaalem3  26301  dvntaylp  26351  ulmss  26378  mtest  26385  sineq0  26504  efif1olem4  26525  cxpexp  26648  mulcxplem  26664  mulcxp  26665  cxpmul2  26669  cxpeq  26737  affineequiv2  26804  quad2  26819  dcubic  26826  leibpi  26922  o1cxp  26955  scvxcvx  26966  facgam  27046  wilthlem1  27048  wilthlem2  27049  mpodvdsmulf1o  27174  fsumdvdsmul  27175  perfect  27211  dchrelbas2  27217  dchrinv  27241  dchrptlem2  27245  lgsne0  27315  lgsqrlem2  27327  lgsdchr  27335  gausslemma2d  27354  lgseisenlem2  27356  lgsquad2lem2  27365  2lgslem1a  27371  2lgslem1b  27372  dchrisumlem1  27469  qabvexp  27606  ostthlem1  27607  ostthlem2  27608  ostth3  27618  ltsval2  27637  ltsres  27643  nolesgn2ores  27653  nogesgn1ores  27655  nolt02o  27676  nogt01o  27677  nosupcbv  27683  nosupno  27684  nosupdm  27685  nosupfv  27687  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1lem3  27691  nosupbnd1lem5  27693  noinfcbv  27698  noinfno  27699  noinfdm  27700  noinffv  27702  noinfres  27703  noinfbnd1lem3  27706  noinfbnd1lem5  27708  addsrid  27973  addscom  27975  addscan1  28003  addsass  28014  subscan1d  28112  subscan2d  28113  mulsrid  28122  mulscom  28148  addsdilem3  28162  addsdilem4  28163  addsdi  28164  mulsasslem3  28174  mulsass  28175  mulscan2d  28188  mulscan1d  28189  bdayons  28285  om2noseqrdg  28313  n0cut  28343  expadds  28444  pw2cut  28469  pw2cut2  28471  elreno  28500  istrkgc  28539  istrkgcb  28541  istrkgld  28544  istrkg2ld  28545  axtgcgrrflx  28547  axtgupdim2  28556  tgjustf  28558  tgjustr  28559  iscgrg  28597  iscgrglt  28599  trgcgrg  28600  tgcgr4  28616  motcgr  28621  legso  28684  mirval  28740  israg  28782  ismidb  28863  isinagd  28924  f1otrgds  28954  ttgval  28960  ttgitvval  28967  brcgr  28986  brbtwn2  28991  colinearalglem1  28992  colinearalg  28996  ax5seglem1  29014  ax5seglem2  29015  ax5seglem8  29022  ax5seglem9  29023  axlowdimlem13  29040  axlowdimlem16  29043  axlowdim1  29045  axcontlem1  29050  axcontlem2  29051  axcontlem6  29055  axcontlem7  29056  axcontlem8  29057  ecgrtg  29069  usgredg2v  29313  issubgr  29357  cplgruvtxb  29499  cusgrsize  29541  finsumvtxdg2size  29637  isrgr  29646  wkslem1  29694  wkslem2  29695  iswlk  29697  uspgr2wlkeq  29732  2wlklem  29752  wlkres  29755  redwlk  29757  wlkp1lem6  29763  wlkp1lem7  29764  wlkp1lem8  29765  pthdivtx  29813  upgrwlkdvdelem  29822  isclwlk  29859  iscrct  29876  iscycl  29877  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  wwlksnextinj  29985  rusgrnumwwlk  30064  clwlkclwwlklem2  30088  clwlkclwwlkf1lem3  30094  clwlkclwwlkf1  30098  erclwwlkeq  30106  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  erclwwlkneq  30155  clwwlkvbij  30201  upgreupthseg  30297  eupth2eucrct  30305  eupth2lem3  30324  eupth2  30327  eucrctshift  30331  2clwwlk  30435  numclwwlk1lem2f1  30445  numclwlk1lem1  30457  numclwlk1lem2  30458  numclwlk2lem2f1o  30467  isgrpo  30586  grpoass  30592  grpoidinvlem3  30595  grpoidinv  30597  grpoideu  30598  grpoidinv2  30604  grpoinvfval  30611  isablo  30635  ablocom  30637  vciOLD  30650  vcidOLD  30653  vcdi  30654  vcdir  30655  vcass  30656  isvclem  30666  isnvlem  30699  nvmeq0  30747  nvs  30752  imsmetlem  30779  islno  30842  lnolin  30843  ishmo  30900  isphg  30906  phpar2  30912  phpar  30913  ipdiri  30919  ipasslem1  30920  ipasslem5  30924  ipasslem11  30929  ipassi  30930  dipdir  30931  dipass  30934  ip2eqi  30945  htth  31007  hvsubsub4  31149  hvnegdi  31156  hvaddcan  31159  hvaddcan2  31160  hvsubcan  31163  hvsubcan2  31164  hvaddsub4  31167  hial2eq  31195  normlem9at  31210  normsq  31223  norm-iii  31229  normsub  31232  normpyth  31234  normpar  31244  polid  31248  issubgoilem  31349  ococ  31495  chj0  31586  chlejb1  31601  chdmm1  31614  chjass  31622  spanun  31634  spansn  31648  elspansn2  31656  cmbr  31673  cmbr3  31697  pjoml2  31700  pjoml3  31701  osum  31734  spansnj  31736  pjch1  31759  pjadji  31774  pjaddi  31775  pjinormi  31776  pjsubi  31777  pjmuli  31778  pjcjt2  31781  pjch  31783  pjopyth  31809  pjpyth  31814  hoaddcom  31863  hoaddass  31871  hocsubdir  31874  hoaddrid  31880  ho0sub  31886  honegsub  31888  adjsym  31922  eigrei  31923  eigre  31924  eigposi  31925  eigorth  31927  ellnop  31947  elhmop  31962  ellnfn  31972  cnvadj  31981  lnopl  32003  unop  32004  hmop  32011  lnfnl  32020  adj1  32022  eleigvec  32046  hoddi  32079  lnopeq0lem2  32095  lnopunilem1  32099  lnopunilem2  32100  lnopunii  32101  elunop2  32102  lnophmi  32107  lnfnmul  32137  cnlnadjlem5  32160  branmfn  32194  bra11  32197  hmopidmchi  32240  hmopidmch  32242  hmopidmpj  32243  pjss2coi  32253  pjssmi  32254  pjssge0i  32255  pjidmco  32270  dfpjop  32271  elpjrn  32279  isst  32302  ishst  32303  hstel2  32308  stj  32324  mdbr  32383  mdi  32384  mdbr3  32386  dmdbr  32388  dmdmd  32389  dmdi  32391  dmdbr3  32394  mddmd2  32398  mdsl1i  32410  chjatom  32446  iuninc  32648  fmptcof2  32748  receqid  32835  bcm1n  32886  fsumiunle  32920  sgnsgn  32932  xmulcand  32998  xrsmulgzz  33087  psgnfzto1st  33184  isfxp  33247  fxpgaeq  33248  isslmd  33281  slmdlema  33282  gsumvsca1  33305  gsumvsca2  33306  urpropd  33310  elrgspnsubrunlem2  33327  erlval  33337  domnpropd  33356  domnlcanOLD  33359  qusvscpbl  33429  nsgqusf1olem3  33493  opprqusdrng  33571  ressply1mon1p  33646  ressply1invg  33647  deg1prod  33661  ply1moneq  33666  psrgsum  33710  psrmonmul  33712  psrmonprod  33714  vietalem  33741  vieta  33742  fedgmul  33794  brfldext  33808  fldextrspunlsplem  33836  extdgfialglem1  33855  bralgext  33860  minplyval  33868  submateq  33972  dispcmp  34022  pstmxmet  34060  cnre2csqlem  34073  mndpluscn  34089  qqhval2  34145  isrrext  34163  esumfzf  34232  esumcvg  34249  esum2dlem  34255  esumiun  34257  ofcfeqd2  34264  ismeas  34362  isrnmeas  34363  measvun  34372  carsgval  34466  inelcarsg  34474  carsgclctunlem1  34480  carsgclctunlem2  34482  pmeasmono  34487  pmeasadd  34488  eulerpartlemgvv  34539  eulerpartlemn  34544  sseqp1  34558  probun  34582  breprexp  34796  istrkg2d  34829  axtgupdim2ALTV  34831  afsval  34834  bnj1385  34993  bnj66  35021  bnj106  35029  bnj155  35040  bnj222  35044  bnj540  35053  bnj591  35072  bnj594  35073  bnj611  35079  bnj893  35089  bnj1000  35102  bnj966  35105  bnj1112  35144  bnj1234  35174  bnj1253  35178  bnj1280  35181  bnj1326  35187  bnj1450  35211  bnj1463  35216  bnj1529  35231  f1resveqaeq  35247  pfxwlk  35325  revwlk  35326  subfacp1lem3  35383  subfacp1lem4  35384  subfacp1lem5  35385  subfacp1lem6  35386  subfacval2  35388  erdszelem9  35400  sconnpht  35430  ptpconn  35434  cvmliftmolem1  35482  cvmliftmolem2  35483  cvmliftlem10  35495  cvmlift2  35517  cvmliftphtlem  35518  satfdm  35570  gonarlem  35595  gonar  35596  goalr  35598  satfdmfmla  35601  prv  35629  mrsubff1  35715  mrsubccat  35719  elmrsubrn  35721  mrsubvrs  35723  elmpst  35737  msrid  35746  msubvrs  35761  sqdivzi  35929  shftvalg  35933  bcprod  35939  bccolsum  35940  iprodefisumlem  35941  faclimlem1  35944  rdgprc  35993  dfrdg2  35994  elwlim  36022  fvsingle  36119  fullfunfv  36148  lineelsb2  36349  rankung  36367  ranksng  36368  rankpwg  36370  opnregcld  36531  cldregopn  36532  neibastop3  36563  weiunval  36663  csbttc  36710  mh-inf3f1  36742  bj-sbeqALT  37226  bj-gabeqis  37264  bj-isclm  37624  rdgeqoa  37703  fvineqsnf1  37743  tan2h  37950  matunitlindflem1  37954  matunitlindflem2  37955  poimirlem9  37967  poimirlem13  37971  poimirlem14  37972  poimirlem16  37974  poimirlem19  37977  broucube  37992  voliunnfl  38002  volsupnfl  38003  cocanfo  38057  upixp  38067  sdclem2  38080  caushft  38099  ismtycnv  38140  ismtyima  38141  ismtybndlem  38144  ismtyres  38146  bfplem2  38161  bfp  38162  isass  38184  opidonOLD  38190  exidu1  38194  cmpidelt  38197  grpoeqdivid  38219  elghomlem2OLD  38224  ghomlinOLD  38226  ghomco  38229  isrngo  38235  rngoid  38240  rngoideu  38241  rngodi  38242  rngodir  38243  rngoass  38244  rngohomval  38302  isrngohom  38303  rngohomadd  38307  rngohommul  38308  iscom2  38333  iscringd  38336  crngocom  38339  crngohomfo  38344  dmncan2  38415  elsymrels4  38977  brredunds  39048  lshpset  39441  lcvexchlem4  39500  lcvexchlem5  39501  lflset  39522  islfl  39523  lfli  39524  islfld  39525  eqlkr3  39564  isopos  39643  oposlem  39645  opcon3b  39659  cmtvalN  39674  omllaw  39706  cvlexchb2  39794  cvlatexchb2  39798  cvlsupr2  39806  4atlem9  40066  4atlem10a  40067  4atlem11a  40070  4atlem12a  40073  4at2  40077  pmapglb2N  40234  pmapglb2xN  40235  paddasslem17  40299  ispsubclN  40400  ispsubcl2N  40410  lhpmod2i2  40501  lhpmod6i1  40502  4atexlemex2  40534  4atex  40539  4atex2-0aOLDN  40541  4atex2-0cOLDN  40543  ldilval  40576  ltrnfset  40580  ltrnset  40581  isltrn  40582  ltrneq2  40611  trnfsetN  40618  trnsetN  40619  istrnN  40620  cdlemd5  40665  cdleme0moN  40688  cdleme0nex  40753  cdleme18d  40758  cdleme31so  40842  cdleme31fv  40853  cdlemg2jlemOLDN  41056  cdlemg2fvlem  41057  cdlemg2klem  41058  istendo  41223  tendovalco  41228  tendoeq2  41237  dicelvalN  41641  dihval  41695  dihcnv11  41738  dihmeetlem13N  41782  dihlspsnat  41796  dochn0nv  41838  dochkrshp4  41852  lpolsetN  41945  lpolsatN  41951  lpolpolsatN  41952  lcfl1lem  41954  lclkrlem2a  41970  lclkrlem2e  41974  lcfls1lem  41997  lclkrs2  42003  lcdfval  42051  lcdval  42052  mapdffval  42089  mapdfval  42090  mapd0  42128  mapdpglem30  42165  mapdhval  42187  mapdheq2  42192  hdmap1vallem  42260  hdmap1val  42261  hdmap1cbv  42265  hdmapval3N  42301  hdmap10  42303  hdmapeq0  42307  hdmap14lem12  42342  hdmap14lem13  42343  hgmapfval  42349  hgmapvs  42354  hgmapvv  42389  hlhilocv  42420  recbothd  42448  lcmineqlem13  42497  isprimroot  42549  primrootsunit1  42553  aks6d1c1p1  42563  aks6d1c1p3  42566  aks6d1c1p4  42567  aks6d1c1p5  42568  evl1gprodd  42573  aks6d1c1rh  42581  aks6d1c2lem3  42582  deg1gprod  42596  deg1pow  42597  sticksstones22  42624  aks6d1c6lem2  42627  aks5lem3a  42645  unitscyglem2  42652  unitscyglem3  42653  unitscyglem4  42654  ccatcan2d  42707  remulcan2d  42712  sumcubes  42762  expeqidd  42774  cxp112d  42790  cxp111d  42791  log11d  42795  sn-addcand  42869  sn-addcan2d  42871  sn-mullid  42885  nn0addcom  42924  renegmulnnass  42927  nn0mulcom  42928  zmulcomlem  42929  cnreeu  42952  abvexp  42994  fiabv  42998  prjsprel  43054  prjcrvfval  43081  flt0  43087  sn-isghm  43123  ismrcd2  43148  ismrc  43150  dvdsrabdioph  43259  fphpdo  43266  rmxypairf1o  43360  monotoddzzfi  43391  monotoddzz  43392  oddcomabszz  43393  rmxdioph  43465  expdiophlem2  43471  dnnumch3  43496  aomclem8  43510  islssfg  43519  unxpwdom3  43544  gicabl  43548  idomodle  43640  fgraphxp  43653  hausgraph  43654  onov0suclim  43723  oaabsb  43743  oaomoencom  43766  oenass  43768  omabs2  43781  tfsconcat0b  43795  nadd1suc  43841  naddonnn  43844  minregex  43982  relexpmulnn  44157  clsk1independent  44494  ntrclsk13  44519  ntrclsk4  44520  imo72b2  44620  grumnud  44734  nzss  44765  caofcan  44771  expgrowth  44783  fsneq  45656  fperiodmullem  45757  uzinico3  46013  fsumf1of  46025  fmuldfeq  46034  fprodexp  46045  fprodabs2  46046  climmulf  46055  climexp  46056  climsuse  46059  climrecf  46060  climaddf  46066  mullimc  46067  limcperiod  46079  neglimc  46096  addlimc  46097  0ellimcdiv  46098  climeldmeqmpt  46117  climfveqmpt  46120  climfveqf  46129  climfveqmpt3  46131  climeldmeqf  46132  climeqf  46137  climeldmeqmpt3  46138  limsupequz  46172  cncfperiod  46328  icccncfext  46336  fperdvper  46368  dvnmptdivc  46387  dvnxpaek  46391  dvnmul  46392  dvmptfprod  46394  dvnprodlem3  46397  itgspltprt  46428  stoweidlem30  46479  stoweidlem48  46497  wallispilem4  46517  wallispi2lem1  46520  wallispi2lem2  46521  fourierdlem50  46605  fourierdlem73  46628  fourierdlem81  46636  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem92  46647  fourierdlem94  46649  fourierdlem97  46652  fourierdlem111  46666  fourierdlem112  46667  fourierdlem113  46668  sge0iunmptlemfi  46862  ismea  46900  meadjuni  46906  meaiuninclem  46929  caragenval  46942  isome  46943  caragensplit  46949  carageniuncllem1  46970  caratheodorylem1  46975  hoidmvlelem3  47046  vonvolmbllem  47109  vonvolmbl  47110  smflimlem3  47222  smflim  47226  smfpimcc  47257  smfsuplem2  47261  fsetsnf1  47515  cfsetsnfsetf1  47522  fcoresf1  47532  csbafv12g  47600  csbaovg  47643  csbafv212g  47682  mod2addne  47833  fargshiftf1  47916  fargshiftfva  47918  prproropf1olem4  47981  fmtnorec2  48021  fmtnoprmfac1lem  48042  fmtnofac1  48048  quad1  48111  requad1  48113  perfectALTV  48214  fpprwppr  48230  nfermltl8rev  48233  nfermltl2rev  48234  nfermltlrev  48235  sbgoldbo  48278  isgrim  48373  grimuhgr  48378  grimcnv  48379  grimco  48380  uhgrimedgi  48381  isuspgrim0  48385  upgrimwlklem5  48392  gricushgr  48408  isubgrgrim  48420  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  clnbgrgrim  48425  grimedg  48426  uspgrlimlem3  48481  uspgrlimlem4  48482  grlimedgclnbgr  48486  grlimgrtrilem2  48493  gpgvtxedg0  48554  gpgvtxedg1  48555  uspgrsprf1  48638  plusfreseq  48655  iscomlaw  48681  isasslaw  48683  lidldomn1  48722  zlidlring  48725  rngcsectALTV  48766  ringcsectALTV  48800  ovmpordxf  48830  lmodvsmdi  48870  islininds  48937  lindslinindimp2lem4  48952  lindslinindsimp2  48954  lmod1  48983  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  nn0sumshdig  49114  1arymaptf1  49133  2arymaptf1  49144  itcovalpc  49163  itcovalt2  49168  rrx2pnecoorneor  49206  rrx2plordisom  49214  rrx2line  49231  rrx2linest  49233  line2ylem  49242  line2x  49245  line2y  49246  itscnhlc0yqe  49250  itscnhlc0xyqsol  49256  idmon  49510  idepi  49511  sectpropdlem  49526  ssccatid  49562  imaidfu  49600  oppff1  49638  imasubc  49641  diag1f1lem  49796  diag2f1lem  49798  fucofvalne  49815  catcsect  49888  grptcmon  50083  grptcepi  50084  aacllem  50291