Theorem eqeq12d 2778

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  neeq12d  3018  cdeqeq  3738  sbceqg  4366  csbun  4395  csbin  4396  csbdif  4479  csbif  4538  iununi  5056  csbopab  5526  csbopabw  5527  dfid2  5544  csbima12  6068  dmsnsnsn  6207  csbcog  6284  dfpred3g  6300  preddowncl  6319  limeq  6358  csbiota  6514  fveqres  6911  opabiota  6949  fvmptf  6997  eqfnfv2f  7015  fsneq  7016  fvreseq0  7019  fveqdmss  7059  fvcofneq  7074  fnressn  7141  fnelfp  7159  fprb  7178  fnprb  7192  fntpb  7193  f1cofveqaeqALT  7242  nvocnv  7265  cocan1  7275  cocan2  7276  2fvcoidd  7281  fliftfun  7296  weniso  7338  csbriota  7368  oveqrspc2v  7423  csbov123  7440  eqfnov  7525  ovmpos  7544  ov2gf  7545  ovmpodxf  7546  caovcomg  7591  caovassg  7594  caovcang  7597  caovcanrd  7599  caovcan  7600  caovdig  7610  caovdirg  7613  caovmo  7633  coof  7684  offveqb  7687  caofid0l  7693  caofid0r  7694  caofidlcan  7698  caofass  7700  caonncan  7704  ordunisuc  7812  onsucuni2  7814  orduninsuc  7823  op1stg  7982  op2ndg  7983  f1o2ndf1  8101  xpord2pred  8125  xpord3pred  8132  poseq  8138  soseq  8139  fnsuppres  8171  csbfrecsg  8265  fpr3g  8266  frrlem1  8267  frrlem12  8278  frrlem13  8279  fpr2a  8283  wfr3g  8300  onfununi  8312  tfrlem1  8346  tfrlem3a  8347  tfrlem5  8350  tfrlem9  8356  tfrlem11  8359  tfrlem12  8360  tfr3  8370  tz7.44-1  8377  tz7.44-2  8378  tz7.44-3  8379  rdglem1  8386  rdg0g  8398  seqomlem1  8421  oalim  8501  omlim  8502  oelim  8503  oa0r  8507  om0r  8508  om1r  8512  oaass  8530  oarec  8531  odi  8548  omass  8549  oelim2  8565  oeoalem  8566  oeoa  8567  oeoelem  8568  oeoe  8569  nna0r  8579  nnacom  8587  nnaass  8592  nndi  8593  nnmass  8594  nnmsucr  8595  nnmcom  8596  oaabs  8618  oaabs2  8619  omabs  8621  naddcllem  8646  naddcom  8653  naddrid  8654  naddass  8667  naddsuc2  8672  naddoa  8673  ecovcom  8805  ecovass  8806  ecovdi  8807  dom2lem  8973  unxpdomlem2  9201  unxpdomlem3  9202  ixpfi2  9293  fipreima  9301  ordiso2  9463  wemaplem1  9494  wemaplem2  9495  wemapsolem  9498  cantnfval2  9624  cantnfp1lem3  9635  oemapvali  9639  cantnflem1c  9642  cantnflem1  9644  wemapwe  9652  rnttrcl  9677  tcvalg  9691  frr3g  9714  frr2  9718  rankvalg  9775  rankonidlem  9786  ranklim  9802  rankuni  9821  updjud  9892  cardprclem  9937  cardprc  9938  carduni  9939  fseqenlem1  9980  fodomacn  10012  alephcard  10026  alephfp2  10065  alephval3  10066  dfac12lem1  10100  dfac12lem2  10101  dfac12r  10103  ackbij1lem8  10182  ackbij1lem14  10188  ackbij1lem16  10190  ackbij2lem3  10196  cardcf  10208  sornom  10234  fin23lem28  10297  isf32lem2  10311  itunitc  10378  ituniiun  10379  axdc3lem2  10408  axdc4lem  10412  ttukeylem3  10468  ttukey2g  10473  fpwwe2lem7  10595  fpwwecbv  10602  canth4  10605  pwfseqlem2  10617  addcanpi  10857  mulcanpi  10858  recrecnq  10925  ltexnq  10933  genpv  10957  0idsr  11055  1idsr  11056  ax1rid  11119  mulrid  11179  addcan  11367  addcan2  11368  mulcand  11820  mulcan2d  11821  mulcan2g  11841  div11OLD  11874  divmuleq  11896  conjmul  11908  eqneg  11911  ofsubeq0  12192  nnadd1com  12236  nnaddcom  12237  nnadddir  12269  nnmul1com  12270  nnmulcom  12271  rpnnen1lem6  12983  cnref1o  12986  xmulasslem  13288  xmulass  13290  xadddi2  13300  prunioo  13485  fzsuc2  13587  fzprval  13590  fztpval  13591  fzosplitprm1  13784  modadd1  13918  modaddb  13919  modmul1  13937  addmodlteq  13959  om2uzsuci  13961  om2uzrdg  13969  uzrdgxfr  13980  seq1  14027  seqp1  14029  seqfveq2  14037  seqfveq  14039  seqshft2  14041  seqsplit  14048  seqcaopr3  14050  seqcaopr2  14051  seqf1olem2a  14053  seqf1olem2  14055  seqf1o  14056  seqid  14060  seqid2  14061  seqhomo  14062  ser1const  14071  seqof2  14073  mulexp  14114  expadd  14117  expmul  14120  binom2  14230  sq01  14238  modexp  14251  bcpasc  14334  hashgadd  14390  hashdom  14392  hashfzo  14442  hashfzp1  14444  hashxplem  14446  hashxp  14447  hashmap  14448  hashpw  14449  hashbclem  14465  hashbc  14466  hashfacen  14467  hashf1lem1  14468  hashf1lem2  14469  hashf1  14470  seqcoll  14477  eqs1  14626  swrdspsleq  14679  pfxeq  14709  pfxsuff1eqwrdeq  14712  ccatopth2  14730  cats1un  14734  swrdccatin1  14738  swrdccat3blem  14752  cshf1  14823  repswcshw  14825  s2eq2s1eq  14949  s3eqs2s1eq  14951  pfx2  14960  2swrd2eqwrdeq  14966  wwlktovf1  14970  eqwrds3  14974  relexpsucnnr  15038  relexpsucnnl  15043  relexpcnv  15048  relexpaddnn  15064  replim  15143  cjreb  15150  cjexp  15177  absexp  15331  abs1m  15363  recan  15364  cnsqrt00  15420  isercoll2  15696  iseraltlem2  15710  iseraltlem3  15711  sumeq2ii  15720  zsum  15745  fsum  15747  fsumf1o  15750  sumss  15751  fsumcvg2  15754  fsumadd  15767  isummulc2  15789  fsum2d  15798  fsummulc2  15811  fsumconst  15817  modfsummods  15821  modfsummod  15822  fsumparts  15834  fsumrelem  15835  fsumiun  15849  binom  15860  bcxmas  15865  incexclem  15866  isumshft  15869  isumnn0nn  15872  climcndslem1  15879  climcndslem2  15880  mertenslem2  15915  clim2prod  15918  prodfrec  15925  prodeq2ii  15941  zprod  15967  fprod  15971  fprodf1o  15976  fprodser  15979  fprodmul  15990  fproddiv  15991  prodsn  15992  prodsnf  15994  fprodabs  16004  fprodconst  16008  fprod2d  16011  fprodmodd  16027  binomfallfac  16071  bpolydif  16085  fprodefsum  16125  efne0d  16127  efne0OLD  16129  efexp  16133  demoivreALT  16233  moddvds  16297  bitsinv1  16476  sadadd2  16494  smu01lem  16519  smupval  16522  smueqlem  16524  smumullem  16526  gcdaddm  16559  bezoutlem1  16573  bezout  16577  gcddiv  16585  seq1st  16605  alginv  16609  algfx  16614  lcmneg  16637  lcmid  16643  lcmgcdeq  16646  lcmfunsnlem1  16671  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem  16675  lcmfunsn  16678  lcmfun  16679  divgcdcoprm0  16699  cncongr1  16701  cncongr2  16702  nn0gcdsq  16787  crth  16813  eulerthlem2  16817  pythagtriplem1  16852  iserodd  16871  pcqmul  16889  pcexp  16895  pcneg  16910  pcmpt  16928  pcfac  16935  prmreclem2  16953  prmreclem3  16954  1arith  16963  vdwpc  17016  ramcl  17065  prmop1  17074  imasval  17541  ercpbllem  17578  iscat  17704  iscatd  17705  catideu  17707  iscatd2  17713  catlid  17715  catrid  17716  catass  17718  homfeq  17726  comfeq  17738  catpropd  17741  moni  17769  epii  17776  sectffval  17783  sectfval  17784  oppcsect  17811  sectmon  17815  isfunc  17897  funcid  17903  funcco  17904  funcpropd  17935  isfull  17945  fthsect  17960  fthmon  17962  natfval  17982  isnat  17983  nati  17991  fucsect  18008  natpropd  18012  setcmon  18120  setcepi  18121  setcsect  18122  fthestrcsetc  18182  embedsetcestrclem  18189  fthsetcestrc  18197  evlfcl  18254  uncfcurf  18271  yoniso  18317  joinval  18407  meetval  18421  islat  18465  latdisdlem  18528  latdisd  18529  isclat  18532  isdlat  18554  dlatmjdi  18555  isacs5lem  18577  acsdrscl  18578  acsficl  18579  isps  18600  mgmidmo  18694  mgmlrid  18701  lidrideqd  18703  lidrididd  18704  grpinvalem  18707  grpinva  18708  gsumvalx  18710  gsumval2  18720  ismgmhm  18730  mgmhmpropd  18732  mgmhmlin  18733  mgmhmeql  18750  issgrp  18754  isnsgrp  18757  sgrpass  18759  sgrp1  18763  issgrpd  18764  sgrppropd  18765  ismndd  18790  mndpropd  18793  imasmnd2  18808  xpsmnd0  18812  mnd1  18813  mnd1id  18814  ismhm  18819  mhmpropd  18826  mhmlin  18827  mhmimalem  18858  mhmeql  18860  gsumccat  18875  gsumwmhm  18879  frmdgsum  18896  symggrplem  18918  smndex1mndlem  18946  smndex1n0mnd  18949  sgrp2rid2  18963  sgrp2nmndlem4  18965  isgrp  18981  grppropd  18993  isgrpd2e  18997  dfgrp2  19004  isgrpid2  19018  grpidd2  19019  grpinvfval  19020  grpinvfvalALT  19021  grpinv11  19049  grpinvpropd  19057  grpidssd  19058  grpinvssd  19059  grpsubrcan  19063  dfgrp3lem  19080  grplactcnv  19085  imasgrp2  19097  mhmlem  19104  mulgnn0p1  19127  mulgaddcom  19140  mulginvcom  19141  mulgneg2  19150  mulgnnass  19151  mulgnn0ass  19152  mulgass  19153  mhmmulg  19157  cyccom  19244  isghm  19256  ghmlin  19261  ghmeql  19279  isga  19331  gagrpid  19334  gaass  19337  galcan  19344  orbsta  19353  cntzfval  19360  elcntz  19362  cntzsnval  19364  elcntzsn  19365  cntzi  19369  resscntz  19373  cntzmhm  19381  gsumwrev  19406  snsymgefmndeq  19435  cayleylem2  19453  symgextf1  19461  gsmsymgreqlem2  19471  gsmsymgreq  19472  symgfixf1  19477  pmtrfrn  19498  odfval  19572  odfvalALT  19573  mndodcong  19582  odbezout  19598  odeq1  19600  submod  19609  gexval  19618  gexdvds  19624  ispgp  19632  sylow1lem1  19638  sylow2alem1  19657  sylow2alem2  19658  sylow2blem2  19661  efgmnvl  19754  efgredlemc  19785  efgredeu  19792  frgpuptinv  19811  frgpup1  19815  frgpup3lem  19817  iscmn  19829  cmnpropd  19831  iscmnd  19834  abladdsub4  19851  submcmn2  19879  qusabl  19905  abl1  19906  imasabl  19916  iscyg  19919  cycsubmcmn  19929  gsum2dlem2  20011  telgsumfzs  20029  dmdprd  20040  dprdval  20045  dprdfcntz  20057  subgdmdprd  20076  dprd2da  20084  dpjrid  20104  pgpfac1lem3a  20118  ablfaclem3  20129  ablfac2  20131  gsumle  20185  isrng  20200  rngdi  20206  rngdir  20207  rngpropd  20220  imasrng  20223  ringurd  20235  issrg  20238  o2timesd  20260  rglcom4d  20261  srgmulgass  20267  srgpcomp  20268  srgbinom  20281  isring  20287  ringpropd  20338  ringinvnz1ne0  20350  mulgass2  20359  ring1  20360  imasring  20379  xpsring1d  20382  dvdsr  20411  dvreq1  20460  rnghmval  20489  isrnghm  20490  rnghmmul  20498  c0snmgmhm  20511  rngisomring1  20517  zrrnghm  20586  islring  20590  rngcsect  20686  ringcsect  20720  rrgval  20747  unitrrg  20753  domnlcanb  20770  domnrcanb  20772  isdrng  20783  drngprop  20794  isdrngd  20815  isdrngdOLD  20817  drngpropd  20819  cntzsdrg  20851  isabv  20860  abvmul  20870  issrng  20893  issrngd  20904  idsrngd  20905  islmod  20931  lmodlema  20932  islmodd  20933  lmodvsmmulgdi  20964  lmodprop2d  20991  rmodislmodlem  20996  rmodislmod  20997  islmhm  21094  lmhmlin  21102  islmhm2  21105  lmhmeql  21122  lmhmpropd  21140  islbs  21143  lbspropd  21166  rnglidlmsgrp  21316  rnglidlrng  21317  quscrng  21353  rngqiprngimfo  21371  islpir  21398  cnfldmulg  21456  cnfldexp  21457  prmirredlem  21524  pzriprnglem6  21538  pzriprnglem10  21542  pzriprnglem12  21544  chrcong  21579  zndvds  21601  znf1o  21603  znunit  21615  cygznlem3  21621  frgpcyg  21625  psgndiflemB  21652  isphl  21680  ipcj  21686  iporthcom  21687  ip2eq  21705  isphld  21706  phlpropd  21707  phlssphl  21711  ocvfval  21718  iscss  21735  ishil  21770  isobs  21772  obsip  21773  obslbs  21782  frlmphl  21833  isassa  21908  assalem  21909  isassad  21917  assapropd  21923  assamulgscm  21953  mvrf1  22037  mplmonmul  22089  mplcoe1  22090  mplcoe3  22091  mplcoe5lem  22092  mplcoe5  22093  evlslem1  22135  mpfrcl  22138  evlsval  22139  psdpw  22235  coe1tm  22336  ply1sclf1  22352  ply1coe  22361  eqcoe1ply1eq  22362  cply1coe0bi  22365  coe1fzgsumd  22367  ply1scleq  22368  ply1chr  22369  gsumply1eq  22372  evl1gsumd  22420  mat0dimcrng  22530  mat1ghm  22543  mat1mhm  22544  dmatcrng  22562  scmateALT  22572  scmatcrng  22581  scmatf1  22591  mvmumamul1  22614  mdetdiagid  22660  mdetralt  22668  mdetunilem1  22672  mdetunilem3  22674  mdetunilem4  22675  mdetunilem7  22678  mdetunilem9  22680  mdetuni0  22681  madugsum  22703  smadiadetr  22735  mat2pmatf1  22789  m2cpminvid2lem  22814  decpmataa0  22828  pmatcollpw2lem  22837  pm2mpf1  22859  chcoeffeqlem  22945  chcoeffeq  22946  cayhamlem3  22947  cayleyhamilton1  22952  isperf  23211  restperf  23244  cmpsub  23460  isconn  23473  2ndcsep  23519  elptr2  23634  ptbasin  23637  dfac14  23678  txcnp  23680  ptcnplem  23681  ptcnp  23682  cnmpt11  23723  cnmpt21  23731  cnmptcom  23738  kqfeq  23784  isr0  23797  pt1hmeo  23866  ustexsym  24276  isusp  24321  imasdsf1olem  24433  isxms  24507  xmspropd  24533  imasf1oxms  24549  stdbdmopn  24578  isngp3  24658  ngppropd  24697  tngngp3  24716  isnlm  24735  nmvs  24736  xrsxmet  24870  cnheibor  25017  htpyi  25036  htpycc  25042  pi1xfr  25117  pi1coghm  25123  isclm  25126  lmhmclm  25149  isclmp  25159  clmmulg  25163  iscph  25232  tcphcph  25299  cphsscph  25313  cmetcaulem  25350  bcth3  25393  ovolunlem1a  25558  ovolicc2lem1  25579  ovolicc2lem4  25582  ovolicc2  25584  mblsplit  25594  volun  25607  volfiniun  25609  voliunlem1  25612  volsup  25618  ioorinv  25638  uniioombllem2  25645  vitalilem3  25672  mbfeqalem1  25703  mbflim  25730  itgeqa  25876  itgconst  25881  itgfsum  25889  itgsplitioo  25900  dvnadd  25991  dvnres  25993  dvexp  26015  dvmptfsum  26037  mvth  26054  dvlip  26055  lhop1lem  26075  dvcvx  26082  mdegle0  26137  ply1nzb  26183  mon1pval  26202  facth1  26227  ig1pval  26236  dgrmulc  26331  dgrcolem1  26333  dgrcolem2  26334  dgrco  26335  coecj  26338  coecjOLD  26340  vieta1lem2  26375  vieta1  26376  elqaalem3  26385  dvntaylp  26434  ulmss  26460  mtest  26467  sineq0  26589  efif1olem4  26610  cxpexp  26733  mulcxplem  26749  mulcxp  26750  cxpmul2  26754  cxpeq  26822  affineequiv2  26889  quad2  26904  dcubic  26911  leibpi  27007  o1cxp  27039  scvxcvx  27050  facgam  27130  wilthlem1  27132  wilthlem2  27133  mpodvdsmulf1o  27258  fsumdvdsmul  27259  perfect  27295  dchrelbas2  27301  dchrinv  27325  dchrptlem2  27329  lgsne0  27399  lgsqrlem2  27411  lgsdchr  27419  gausslemma2d  27438  lgseisenlem2  27440  lgsquad2lem2  27449  2lgslem1a  27455  2lgslem1b  27456  dchrisumlem1  27553  qabvexp  27690  ostthlem1  27691  ostthlem2  27692  ostth3  27702  ltsval2  27720  ltsres  27726  nolesgn2ores  27736  nogesgn1ores  27738  nolt02o  27759  nogt01o  27760  nosupcbv  27766  nosupno  27767  nosupdm  27768  nosupfv  27770  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  noinfcbv  27781  noinfno  27782  noinfdm  27783  noinffv  27785  noinfres  27786  noinfbnd1lem3  27789  noinfbnd1lem5  27791  addsrid  28057  addscom  28059  addscan1  28087  addsass  28098  subscan1d  28196  subscan2d  28197  mulsrid  28206  mulscom  28232  addsdilem3  28246  addsdilem4  28247  addsdi  28248  mulsasslem3  28258  mulsass  28259  mulscan2d  28272  mulscan1d  28273  bdayons  28369  om2noseqrdg  28397  n0cut  28427  expadds  28528  pw2cut  28553  pw2cut2  28555  elreno  28584  istrkgc  28623  istrkgcb  28625  istrkgld  28628  istrkg2ld  28629  axtgcgrrflx  28631  axtgupdim2  28640  tgjustf  28642  tgjustr  28643  iscgrg  28681  iscgrglt  28683  trgcgrg  28684  tgcgr4  28700  motcgr  28705  legso  28768  mirval  28828  israg  28870  ismidb  28951  isinagd  29033  f1otrgds  29069  ttgval  29075  ttgitvval  29082  brcgr  29101  brbtwn2  29106  colinearalglem1  29107  colinearalg  29111  ax5seglem1  29129  ax5seglem2  29130  ax5seglem8  29137  ax5seglem9  29138  axlowdimlem13  29155  axlowdimlem16  29158  axlowdim1  29160  axcontlem1  29165  axcontlem2  29166  axcontlem6  29170  axcontlem7  29171  axcontlem8  29172  ecgrtg  29184  usgredg2v  29428  issubgr  29472  cplgruvtxb  29614  cusgrsize  29655  finsumvtxdg2size  29751  isrgr  29760  wkslem1  29808  wkslem2  29809  iswlk  29811  uspgr2wlkeq  29846  2wlklem  29866  wlkres  29869  redwlk  29871  wlkp1lem6  29877  wlkp1lem7  29878  wlkp1lem8  29879  pthdivtx  29927  upgrwlkdvdelem  29936  isclwlk  29973  iscrct  29990  iscycl  29991  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  crctcshwlkn0lem6  30015  wwlksnextinj  30099  rusgrnumwwlk  30178  clwlkclwwlklem2  30202  clwlkclwwlkf1lem3  30208  clwlkclwwlkf1  30212  erclwwlkeq  30220  clwwlkel  30248  clwwlkf  30249  clwwlkf1  30251  erclwwlkneq  30269  clwwlkvbij  30315  upgreupthseg  30411  eupth2eucrct  30419  eupth2lem3  30438  eupth2  30441  eucrctshift  30445  2clwwlk  30549  numclwwlk1lem2f1  30559  numclwlk1lem1  30571  numclwlk1lem2  30572  numclwlk2lem2f1o  30581  isgrpo  30700  grpoass  30706  grpoidinvlem3  30709  grpoidinv  30711  grpoideu  30712  grpoidinv2  30718  grpoinvfval  30725  isablo  30749  ablocom  30751  vciOLD  30764  vcidOLD  30767  vcdi  30768  vcdir  30769  vcass  30770  isvclem  30780  isnvlem  30813  nvmeq0  30861  nvs  30866  imsmetlem  30893  islno  30956  lnolin  30957  ishmo  31014  isphg  31020  phpar2  31026  phpar  31027  ipdiri  31033  ipasslem1  31034  ipasslem5  31038  ipasslem11  31043  ipassi  31044  dipdir  31045  dipass  31048  ip2eqi  31059  htth  31121  hvsubsub4  31263  hvnegdi  31270  hvaddcan  31273  hvaddcan2  31274  hvsubcan  31277  hvsubcan2  31278  hvaddsub4  31281  hial2eq  31309  normlem9at  31324  normsq  31337  norm-iii  31343  normsub  31346  normpyth  31348  normpar  31358  polid  31362  issubgoilem  31463  ococ  31609  chj0  31700  chlejb1  31715  chdmm1  31728  chjass  31736  spanun  31748  spansn  31762  elspansn2  31770  cmbr  31787  cmbr3  31811  pjoml2  31814  pjoml3  31815  osum  31848  spansnj  31850  pjch1  31873  pjadji  31888  pjaddi  31889  pjinormi  31890  pjsubi  31891  pjmuli  31892  pjcjt2  31895  pjch  31897  pjopyth  31923  pjpyth  31928  hoaddcom  31977  hoaddass  31985  hocsubdir  31988  hoaddrid  31994  ho0sub  32000  honegsub  32002  adjsym  32036  eigrei  32037  eigre  32038  eigposi  32039  eigorth  32041  ellnop  32061  elhmop  32076  ellnfn  32086  cnvadj  32095  lnopl  32117  unop  32118  hmop  32125  lnfnl  32134  adj1  32136  eleigvec  32160  hoddi  32193  lnopeq0lem2  32209  lnopunilem1  32213  lnopunilem2  32214  lnopunii  32215  elunop2  32216  lnophmi  32221  lnfnmul  32251  cnlnadjlem5  32274  branmfn  32308  bra11  32311  hmopidmchi  32354  hmopidmch  32356  hmopidmpj  32357  pjss2coi  32367  pjssmi  32368  pjssge0i  32369  pjidmco  32384  dfpjop  32385  elpjrn  32393  isst  32416  ishst  32417  hstel2  32422  stj  32438  mdbr  32497  mdi  32498  mdbr3  32500  dmdbr  32502  dmdmd  32503  dmdi  32505  dmdbr3  32508  mddmd2  32512  mdsl1i  32524  chjatom  32560  iuninc  32760  fmptcof2  32859  receqid  32946  bcm1n  32997  fsumiunle  33031  sgnsgn  33033  xmulcand  33098  xrsmulgzz  33187  psgnfzto1st  33285  isfxp  33348  fxpgaeq  33349  isslmd  33382  slmdlema  33383  gsumvsca1  33406  gsumvsca2  33407  urpropd  33411  elrgspnsubrunlem2  33429  erlval  33439  domnpropd  33461  domnlcanOLD  33464  qusvscpbl  33537  nsgqusf1olem3  33601  opprqusdrng  33681  ressply1mon1p  33764  ressply1invg  33765  deg1prod  33779  ply1moneq  33784  psrgsum  33845  psrmonmul  33847  psrmonprod  33849  vietalem  33876  vieta  33877  fedgmul  33928  brfldext  33942  fldextrspunlsplem  33970  extdgfialglem1  33989  bralgext  33994  minplyval  34002  submateq  34106  dispcmp  34156  pstmxmet  34194  cnre2csqlem  34207  mndpluscn  34223  qqhval2  34279  isrrext  34297  esumfzf  34366  esumcvg  34383  esum2dlem  34389  esumiun  34391  ofcfeqd2  34398  ismeas  34496  isrnmeas  34497  measvun  34506  carsgval  34600  inelcarsg  34608  carsgclctunlem1  34614  carsgclctunlem2  34616  pmeasmono  34621  pmeasadd  34622  eulerpartlemgvv  34673  eulerpartlemn  34678  sseqp1  34692  probun  34716  breprexp  34927  istrkg2d  34960  axtgupdim2ALTV  34962  afsval  34968  bnj1385  35127  bnj66  35155  bnj106  35163  bnj155  35174  bnj222  35178  bnj540  35187  bnj591  35206  bnj594  35207  bnj611  35213  bnj893  35223  bnj1000  35236  bnj966  35239  bnj1112  35278  bnj1234  35308  bnj1253  35312  bnj1280  35315  bnj1326  35321  bnj1450  35345  bnj1463  35350  bnj1529  35365  f1resveqaeq  35379  pfxwlk  35474  revwlk  35475  subfacp1lem3  35532  subfacp1lem4  35533  subfacp1lem5  35534  subfacp1lem6  35535  subfacval2  35537  erdszelem9  35549  sconnpht  35579  ptpconn  35583  cvmliftmolem1  35631  cvmliftmolem2  35632  cvmliftlem10  35644  cvmlift2  35666  cvmliftphtlem  35667  satfdm  35719  gonarlem  35744  gonar  35745  goalr  35747  satfdmfmla  35750  prv  35778  mrsubff1  35864  mrsubccat  35868  elmrsubrn  35870  mrsubvrs  35872  elmpst  35886  msrid  35895  msubvrs  35910  sqdivzi  36078  shftvalg  36082  bcprod  36088  bccolsum  36089  iprodefisumlem  36090  faclimlem1  36093  rdgprc  36142  dfrdg2  36143  elwlim  36171  fvsingle  36268  fullfunfv  36297  lineelsb2  36498  rankung  36516  ranksng  36517  rankpwg  36519  nmulprop  36540  nmulcom  36544  opnregcld  36690  cldregopn  36691  neibastop3  36722  weiunval  36822  csbttc  36869  mh-inf3f1  36901  bj-sbeqALT  37385  bj-gabeqis  37423  bj-isclm  37783  rdgeqoa  37864  fvineqsnf1  37904  tan2h  38111  matunitlindflem1  38115  matunitlindflem2  38116  poimirlem9  38128  poimirlem13  38132  poimirlem14  38133  poimirlem16  38135  poimirlem19  38138  broucube  38153  voliunnfl  38163  volsupnfl  38164  cocanfo  38218  upixp  38228  sdclem2  38241  caushft  38260  ismtycnv  38301  ismtyima  38302  ismtybndlem  38305  ismtyres  38307  bfplem2  38322  bfp  38323  isass  38345  opidonOLD  38351  exidu1  38355  cmpidelt  38358  grpoeqdivid  38380  elghomlem2OLD  38385  ghomlinOLD  38387  ghomco  38390  isrngo  38396  rngoid  38401  rngoideu  38402  rngodi  38403  rngodir  38404  rngoass  38405  rngohomval  38463  isrngohom  38464  rngohomadd  38468  rngohommul  38469  iscom2  38494  iscringd  38497  crngocom  38500  crngohomfo  38505  dmncan2  38576  elsymrels4  39138  brredunds  39209  lshpset  39602  lcvexchlem4  39661  lcvexchlem5  39662  lflset  39683  islfl  39684  lfli  39685  islfld  39686  eqlkr3  39725  isopos  39804  oposlem  39806  opcon3b  39820  cmtvalN  39835  omllaw  39867  cvlexchb2  39955  cvlatexchb2  39959  cvlsupr2  39967  4atlem9  40227  4atlem10a  40228  4atlem11a  40231  4atlem12a  40234  4at2  40238  pmapglb2N  40395  pmapglb2xN  40396  paddasslem17  40460  ispsubclN  40561  ispsubcl2N  40571  lhpmod2i2  40662  lhpmod6i1  40663  4atexlemex2  40695  4atex  40700  4atex2-0aOLDN  40702  4atex2-0cOLDN  40704  ldilval  40737  ltrnfset  40741  ltrnset  40742  isltrn  40743  ltrneq2  40772  trnfsetN  40779  trnsetN  40780  istrnN  40781  cdlemd5  40826  cdleme0moN  40849  cdleme0nex  40914  cdleme18d  40919  cdleme31so  41003  cdleme31fv  41014  cdlemg2jlemOLDN  41217  cdlemg2fvlem  41218  cdlemg2klem  41219  istendo  41384  tendovalco  41389  tendoeq2  41398  dicelvalN  41802  dihval  41856  dihcnv11  41899  dihmeetlem13N  41943  dihlspsnat  41957  dochn0nv  41999  dochkrshp4  42013  lpolsetN  42106  lpolsatN  42112  lpolpolsatN  42113  lcfl1lem  42115  lclkrlem2a  42131  lclkrlem2e  42135  lcfls1lem  42158  lclkrs2  42164  lcdfval  42212  lcdval  42213  mapdffval  42250  mapdfval  42251  mapd0  42289  mapdpglem30  42326  mapdhval  42348  mapdheq2  42353  hdmap1vallem  42421  hdmap1val  42422  hdmap1cbv  42426  hdmapval3N  42462  hdmap10  42464  hdmapeq0  42468  hdmap14lem12  42503  hdmap14lem13  42504  hgmapfval  42510  hgmapvs  42515  hgmapvv  42550  hlhilocv  42581  recbothd  42609  lcmineqlem13  42658  isprimroot  42710  primrootsunit1  42714  aks6d1c1p1  42724  aks6d1c1p3  42727  aks6d1c1p4  42728  aks6d1c1p5  42729  evl1gprodd  42734  aks6d1c1rh  42742  aks6d1c2lem3  42743  deg1gprod  42757  deg1pow  42758  sticksstones22  42785  aks6d1c6lem2  42788  aks5lem3a  42806  unitscyglem2  42813  unitscyglem3  42814  unitscyglem4  42815  ccatcan2d  42867  remulcan2d  42872  sumcubes  42922  expeqidd  42934  cxp112d  42950  cxp111d  42951  log11d  42955  sn-addcand  43029  sn-addcan2d  43031  sn-mullid  43045  nn0addcom  43084  renegmulnnass  43087  nn0mulcom  43088  zmulcomlem  43089  cnreeu  43112  abvexp  43150  fiabv  43154  prjsprel  43186  prjcrvfval  43213  flt0  43219  sn-isghm  43255  ismrcd2  43280  ismrc  43282  dvdsrabdioph  43387  fphpdo  43394  rmxypairf1o  43488  monotoddzzfi  43519  monotoddzz  43520  oddcomabszz  43521  rmxdioph  43593  expdiophlem2  43599  dnnumch3  43624  aomclem8  43638  islssfg  43647  unxpwdom3  43672  gicabl  43676  idomodle  43768  fgraphxp  43781  hausgraph  43782  onov0suclim  43851  oaabsb  43871  oaomoencom  43894  oenass  43896  omabs2  43909  tfsconcat0b  43923  nadd1suc  43969  naddonnn  43972  minregex  44110  relexpmulnn  44285  clsk1independent  44622  ntrclsk13  44647  ntrclsk4  44648  imo72b2  44748  grumnud  44862  nzss  44893  caofcan  44899  expgrowth  44911  fperiodmullem  45882  uzinico3  46138  fsumf1of  46150  fmuldfeq  46159  fprodexp  46170  fprodabs2  46171  climmulf  46180  climexp  46181  climsuse  46184  climrecf  46185  climaddf  46191  mullimc  46192  limcperiod  46204  neglimc  46221  addlimc  46222  0ellimcdiv  46223  climeldmeqmpt  46242  climfveqmpt  46245  climfveqf  46254  climfveqmpt3  46256  climeldmeqf  46257  climeqf  46262  climeldmeqmpt3  46263  limsupequz  46297  cncfperiod  46453  icccncfext  46461  fperdvper  46493  dvnmptdivc  46512  dvnxpaek  46516  dvnmul  46517  dvmptfprod  46519  dvnprodlem3  46522  itgspltprt  46553  stoweidlem30  46604  stoweidlem48  46622  wallispilem4  46642  wallispi2lem1  46645  wallispi2lem2  46646  fourierdlem50  46730  fourierdlem73  46753  fourierdlem81  46761  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem92  46772  fourierdlem94  46774  fourierdlem97  46777  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  sge0iunmptlemfi  46987  ismea  47025  meadjuni  47031  meaiuninclem  47054  caragenval  47067  isome  47068  caragensplit  47074  carageniuncllem1  47095  caratheodorylem1  47100  hoidmvlelem3  47171  vonvolmbllem  47234  vonvolmbl  47235  smflimlem3  47347  smflim  47351  smfpimcc  47382  smfsuplem2  47386  fsetsnf1  47646  cfsetsnfsetf1  47653  fcoresf1  47663  csbafv12g  47731  csbaovg  47774  csbafv212g  47813  mod2addne  47964  fargshiftf1  48047  fargshiftfva  48049  prproropf1olem4  48112  fmtnorec2  48152  fmtnoprmfac1lem  48173  fmtnofac1  48179  quad1  48242  requad1  48244  perfectALTV  48345  fpprwppr  48361  nfermltl8rev  48364  nfermltl2rev  48365  nfermltlrev  48366  sbgoldbo  48409  isgrim  48504  grimuhgr  48509  grimcnv  48510  grimco  48511  uhgrimedgi  48512  isuspgrim0  48516  upgrimwlklem5  48523  gricushgr  48539  isubgrgrim  48551  uhgrimisgrgriclem  48552  clnbgrgrimlem  48555  clnbgrgrim  48556  grimedg  48557  uspgrlimlem3  48612  uspgrlimlem4  48613  grlimedgclnbgr  48617  grlimgrtrilem2  48624  gpgvtxedg0  48685  gpgvtxedg1  48686  uspgrsprf1  48769  plusfreseq  48786  iscomlaw  48812  isasslaw  48814  lidldomn1  48853  zlidlring  48856  rngcsectALTV  48897  ringcsectALTV  48931  ovmpordxf  48961  lmodvsmdi  49001  islininds  49068  lindslinindimp2lem4  49083  lindslinindsimp2  49085  lmod1  49114  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdiglem1  49243  nn0sumshdig  49245  1arymaptf1  49264  2arymaptf1  49275  itcovalpc  49294  itcovalt2  49299  rrx2pnecoorneor  49337  rrx2plordisom  49345  rrx2line  49362  rrx2linest  49364  line2ylem  49373  line2x  49376  line2y  49377  itscnhlc0yqe  49381  itscnhlc0xyqsol  49387  idmon  49641  idepi  49642  sectpropdlem  49657  ssccatid  49693  imaidfu  49731  oppff1  49769  imasubc  49772  diag1f1lem  49927  diag2f1lem  49929  fucofvalne  49946  catcsect  50019  grptcmon  50214  grptcepi  50215  aacllem  50422