Theorem eqeq12d 2755

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  neeq12d  2995  cdeqeq  3716  sbceqg  4340  csbun  4369  csbin  4370  csbdif  4453  csbif  4512  iununi  5028  csbopab  5497  csbopabgALT  5498  dfid2  5515  csbima12  6031  dmsnsnsn  6171  csbcog  6248  dfpred3g  6264  preddowncl  6283  limeq  6322  csbiota  6478  fveqres  6871  opabiota  6909  fvmptf  6957  eqfnfv2f  6975  fsneq  6976  fvreseq0  6979  fveqdmss  7019  fvcofneq  7034  fnressn  7101  fnelfp  7119  fprb  7138  fnprb  7152  fntpb  7153  f1cofveqaeqALT  7202  nvocnv  7225  cocan1  7235  cocan2  7236  2fvcoidd  7241  fliftfun  7256  weniso  7298  csbriota  7328  oveqrspc2v  7383  csbov123  7400  eqfnov  7485  ovmpos  7504  ov2gf  7505  ovmpodxf  7506  caovcomg  7551  caovassg  7554  caovcang  7557  caovcanrd  7559  caovcan  7560  caovdig  7570  caovdirg  7573  caovmo  7593  coof  7644  offveqb  7647  caofid0l  7653  caofid0r  7654  caofidlcan  7658  caofass  7660  caonncan  7664  ordunisuc  7772  onsucuni2  7774  orduninsuc  7783  op1stg  7943  op2ndg  7944  f1o2ndf1  8061  xpord2pred  8085  xpord3pred  8092  poseq  8098  soseq  8099  fnsuppres  8131  csbfrecsg  8224  fpr3g  8225  frrlem1  8226  frrlem12  8237  frrlem13  8238  fpr2a  8242  wfr3g  8259  onfununi  8271  tfrlem1  8305  tfrlem3a  8306  tfrlem5  8309  tfrlem9  8314  tfrlem11  8317  tfrlem12  8318  tfr3  8328  tz7.44-1  8335  tz7.44-2  8336  tz7.44-3  8337  rdglem1  8344  rdg0g  8356  seqomlem1  8379  oalim  8457  omlim  8458  oelim  8459  oa0r  8463  om0r  8464  om1r  8468  oaass  8486  oarec  8487  odi  8504  omass  8505  oelim2  8521  oeoalem  8522  oeoa  8523  oeoelem  8524  oeoe  8525  nna0r  8535  nnacom  8543  nnaass  8548  nndi  8549  nnmass  8550  nnmsucr  8551  nnmcom  8552  oaabs  8574  oaabs2  8575  omabs  8577  naddcllem  8602  naddcom  8608  naddrid  8609  naddass  8622  naddsuc2  8627  naddoa  8628  ecovcom  8760  ecovass  8761  ecovdi  8762  dom2lem  8929  unxpdomlem2  9157  unxpdomlem3  9158  ixpfi2  9250  fipreima  9258  ordiso2  9420  wemaplem1  9451  wemaplem2  9452  wemapsolem  9455  cantnfval2  9581  cantnfp1lem3  9592  oemapvali  9596  cantnflem1c  9599  cantnflem1  9601  wemapwe  9609  rnttrcl  9634  tcvalg  9648  frr3g  9671  frr2  9675  rankvalg  9732  rankonidlem  9743  ranklim  9759  rankuni  9778  updjud  9849  cardprclem  9894  cardprc  9895  carduni  9896  fseqenlem1  9937  fodomacn  9969  alephcard  9983  alephfp2  10022  alephval3  10023  dfac12lem1  10057  dfac12lem2  10058  dfac12r  10060  ackbij1lem8  10139  ackbij1lem14  10145  ackbij1lem16  10147  ackbij2lem3  10153  cardcf  10165  sornom  10190  fin23lem28  10253  isf32lem2  10267  itunitc  10334  ituniiun  10335  axdc3lem2  10364  axdc4lem  10368  ttukeylem3  10424  ttukey2g  10429  fpwwe2lem7  10551  fpwwecbv  10558  canth4  10561  pwfseqlem2  10573  addcanpi  10813  mulcanpi  10814  recrecnq  10881  ltexnq  10889  genpv  10913  0idsr  11011  1idsr  11012  ax1rid  11075  mulrid  11133  addcan  11321  addcan2  11322  mulcand  11774  mulcan2d  11775  mulcan2g  11795  div11OLD  11829  divmuleq  11851  conjmul  11863  eqneg  11866  ofsubeq0  12147  nnadd1com  12191  nnaddcom  12192  nnadddir  12224  nnmul1com  12225  nnmulcom  12226  rpnnen1lem6  12923  cnref1o  12926  xmulasslem  13228  xmulass  13230  xadddi2  13240  prunioo  13425  fzsuc2  13527  fzprval  13530  fztpval  13531  fzosplitprm1  13724  modadd1  13858  modaddb  13859  modmul1  13877  addmodlteq  13899  om2uzsuci  13901  om2uzrdg  13909  uzrdgxfr  13920  seq1  13967  seqp1  13969  seqfveq2  13977  seqfveq  13979  seqshft2  13981  seqsplit  13988  seqcaopr3  13990  seqcaopr2  13991  seqf1olem2a  13993  seqf1olem2  13995  seqf1o  13996  seqid  14000  seqid2  14001  seqhomo  14002  ser1const  14011  seqof2  14013  mulexp  14054  expadd  14057  expmul  14060  binom2  14170  sq01  14178  modexp  14191  bcpasc  14274  hashgadd  14330  hashdom  14332  hashfzo  14382  hashfzp1  14384  hashxplem  14386  hashxp  14387  hashmap  14388  hashpw  14389  hashbclem  14405  hashbc  14406  hashfacen  14407  hashf1lem1  14408  hashf1lem2  14409  hashf1  14410  seqcoll  14417  eqs1  14566  swrdspsleq  14619  pfxeq  14649  pfxsuff1eqwrdeq  14652  ccatopth2  14670  cats1un  14674  swrdccatin1  14678  swrdccat3blem  14692  cshf1  14763  repswcshw  14765  s2eq2s1eq  14889  s3eqs2s1eq  14891  pfx2  14900  2swrd2eqwrdeq  14906  wwlktovf1  14910  eqwrds3  14914  relexpsucnnr  14978  relexpsucnnl  14983  relexpcnv  14988  relexpaddnn  15004  replim  15069  cjreb  15076  cjexp  15103  absexp  15257  abs1m  15289  recan  15290  cnsqrt00  15346  isercoll2  15622  iseraltlem2  15636  iseraltlem3  15637  sumeq2ii  15646  zsum  15671  fsum  15673  fsumf1o  15676  sumss  15677  fsumcvg2  15680  fsumadd  15693  isummulc2  15715  fsum2d  15724  fsummulc2  15737  fsumconst  15743  modfsummods  15747  modfsummod  15748  fsumparts  15760  fsumrelem  15761  fsumiun  15775  binom  15786  bcxmas  15791  incexclem  15792  isumshft  15795  isumnn0nn  15798  climcndslem1  15805  climcndslem2  15806  mertenslem2  15841  clim2prod  15844  prodfrec  15851  prodeq2ii  15867  zprod  15893  fprod  15897  fprodf1o  15902  fprodser  15905  fprodmul  15916  fproddiv  15917  prodsn  15918  prodsnf  15920  fprodabs  15930  fprodconst  15934  fprod2d  15937  fprodmodd  15953  binomfallfac  15997  bpolydif  16011  fprodefsum  16051  efne0d  16053  efne0OLD  16055  efexp  16059  demoivreALT  16159  moddvds  16223  bitsinv1  16402  sadadd2  16420  smu01lem  16445  smupval  16448  smueqlem  16450  smumullem  16452  gcdaddm  16485  bezoutlem1  16499  bezout  16503  gcddiv  16511  seq1st  16531  alginv  16535  algfx  16540  lcmneg  16563  lcmid  16569  lcmgcdeq  16572  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem  16601  lcmfunsn  16604  lcmfun  16605  divgcdcoprm0  16625  cncongr1  16627  cncongr2  16628  nn0gcdsq  16713  crth  16739  eulerthlem2  16743  pythagtriplem1  16778  iserodd  16797  pcqmul  16815  pcexp  16821  pcneg  16836  pcmpt  16854  pcfac  16861  prmreclem2  16879  prmreclem3  16880  1arith  16889  vdwpc  16942  ramcl  16991  prmop1  17000  imasval  17466  ercpbllem  17503  iscat  17629  iscatd  17630  catideu  17632  iscatd2  17638  catlid  17640  catrid  17641  catass  17643  homfeq  17651  comfeq  17663  catpropd  17666  moni  17694  epii  17701  sectffval  17708  sectfval  17709  oppcsect  17736  sectmon  17740  isfunc  17822  funcid  17828  funcco  17829  funcpropd  17860  isfull  17870  fthsect  17885  fthmon  17887  natfval  17907  isnat  17908  nati  17916  fucsect  17933  natpropd  17937  setcmon  18045  setcepi  18046  setcsect  18047  fthestrcsetc  18107  embedsetcestrclem  18114  fthsetcestrc  18122  evlfcl  18179  uncfcurf  18196  yoniso  18242  joinval  18332  meetval  18346  islat  18390  latdisdlem  18453  latdisd  18454  isclat  18457  isdlat  18479  dlatmjdi  18480  isacs5lem  18502  acsdrscl  18503  acsficl  18504  isps  18525  mgmidmo  18619  mgmlrid  18626  lidrideqd  18628  lidrididd  18629  grpinvalem  18632  grpinva  18633  gsumvalx  18635  gsumval2  18645  ismgmhm  18655  mgmhmpropd  18657  mgmhmlin  18658  mgmhmeql  18675  issgrp  18679  isnsgrp  18682  sgrpass  18684  sgrp1  18688  issgrpd  18689  sgrppropd  18690  ismndd  18715  mndpropd  18718  imasmnd2  18733  xpsmnd0  18737  mnd1  18738  mnd1id  18739  ismhm  18744  mhmpropd  18751  mhmlin  18752  mhmimalem  18783  mhmeql  18785  gsumccat  18800  gsumwmhm  18804  frmdgsum  18821  symggrplem  18843  smndex1mndlem  18871  smndex1n0mnd  18874  sgrp2rid2  18888  sgrp2nmndlem4  18890  isgrp  18906  grppropd  18918  isgrpd2e  18922  dfgrp2  18929  isgrpid2  18943  grpidd2  18944  grpinvfval  18945  grpinvfvalALT  18946  grpinv11  18974  grpinvpropd  18982  grpidssd  18983  grpinvssd  18984  grpsubrcan  18988  dfgrp3lem  19005  grplactcnv  19010  imasgrp2  19022  mhmlem  19029  mulgnn0p1  19052  mulgaddcom  19065  mulginvcom  19066  mulgneg2  19075  mulgnnass  19076  mulgnn0ass  19077  mulgass  19078  mhmmulg  19082  cyccom  19169  isghm  19181  isghmOLD  19182  ghmlin  19187  ghmeql  19205  isga  19257  gagrpid  19260  gaass  19263  galcan  19270  orbsta  19279  cntzfval  19286  elcntz  19288  cntzsnval  19290  elcntzsn  19291  cntzi  19295  resscntz  19299  cntzmhm  19307  gsumwrev  19332  snsymgefmndeq  19361  cayleylem2  19379  symgextf1  19387  gsmsymgreqlem2  19397  gsmsymgreq  19398  symgfixf1  19403  pmtrfrn  19424  odfval  19498  odfvalALT  19499  mndodcong  19508  odbezout  19524  odeq1  19526  submod  19535  gexval  19544  gexdvds  19550  ispgp  19558  sylow1lem1  19564  sylow2alem1  19583  sylow2alem2  19584  sylow2blem2  19587  efgmnvl  19680  efgredlemc  19711  efgredeu  19718  frgpuptinv  19737  frgpup1  19741  frgpup3lem  19743  iscmn  19755  cmnpropd  19757  iscmnd  19760  abladdsub4  19777  submcmn2  19805  qusabl  19831  abl1  19832  imasabl  19842  iscyg  19845  cycsubmcmn  19855  gsum2dlem2  19937  telgsumfzs  19955  dmdprd  19966  dprdval  19971  dprdfcntz  19983  subgdmdprd  20002  dprd2da  20010  dpjrid  20030  pgpfac1lem3a  20044  ablfaclem3  20055  ablfac2  20057  gsumle  20111  isrng  20126  rngdi  20132  rngdir  20133  rngpropd  20146  imasrng  20149  ringurd  20157  issrg  20160  o2timesd  20182  rglcom4d  20183  srgmulgass  20189  srgpcomp  20190  srgbinom  20203  isring  20209  ringpropd  20260  ringinvnz1ne0  20272  mulgass2  20281  ring1  20282  imasring  20301  xpsring1d  20304  dvdsr  20333  dvreq1  20382  rnghmval  20411  isrnghm  20412  rnghmmul  20420  c0snmgmhm  20433  rngisomring1  20439  zrrnghm  20508  islring  20512  rngcsect  20608  ringcsect  20642  rrgval  20669  unitrrg  20675  domnlcanb  20692  domnrcanb  20694  isdrng  20705  drngprop  20716  isdrngd  20737  isdrngdOLD  20739  drngpropd  20741  cntzsdrg  20774  isabv  20783  abvmul  20793  issrng  20816  issrngd  20827  idsrngd  20828  islmod  20854  lmodlema  20855  islmodd  20856  lmodvsmmulgdi  20887  lmodprop2d  20914  rmodislmodlem  20919  rmodislmod  20920  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  21379  cnfldexp  21380  prmirredlem  21447  pzriprnglem6  21461  pzriprnglem10  21465  pzriprnglem12  21467  chrcong  21502  zndvds  21524  znf1o  21526  znunit  21538  cygznlem3  21544  frgpcyg  21548  psgndiflemB  21575  isphl  21603  ipcj  21609  iporthcom  21610  ip2eq  21628  isphld  21629  phlpropd  21630  phlssphl  21634  ocvfval  21641  iscss  21658  ishil  21693  isobs  21695  obsip  21696  obslbs  21705  frlmphl  21756  isassa  21831  assalem  21832  isassad  21840  assapropd  21846  assamulgscm  21876  mvrf1  21960  mplmonmul  22012  mplcoe1  22013  mplcoe3  22014  mplcoe5lem  22015  mplcoe5  22016  evlslem1  22058  mpfrcl  22061  evlsval  22062  psdpw  22158  coe1tm  22259  ply1sclf1  22275  ply1coe  22284  eqcoe1ply1eq  22285  cply1coe0bi  22288  coe1fzgsumd  22290  ply1scleq  22291  ply1chr  22292  gsumply1eq  22295  evl1gsumd  22343  mat0dimcrng  22453  mat1ghm  22466  mat1mhm  22467  dmatcrng  22485  scmateALT  22495  scmatcrng  22504  scmatf1  22514  mvmumamul1  22537  mdetdiagid  22583  mdetralt  22591  mdetunilem1  22595  mdetunilem3  22597  mdetunilem4  22598  mdetunilem7  22601  mdetunilem9  22603  mdetuni0  22604  madugsum  22626  smadiadetr  22658  mat2pmatf1  22712  m2cpminvid2lem  22737  decpmataa0  22751  pmatcollpw2lem  22760  pm2mpf1  22782  chcoeffeqlem  22868  chcoeffeq  22869  cayhamlem3  22870  cayleyhamilton1  22875  isperf  23134  restperf  23167  cmpsub  23383  isconn  23396  2ndcsep  23442  elptr2  23557  ptbasin  23560  dfac14  23601  txcnp  23603  ptcnplem  23604  ptcnp  23605  cnmpt11  23646  cnmpt21  23654  cnmptcom  23661  kqfeq  23707  isr0  23720  pt1hmeo  23789  ustexsym  24199  isusp  24244  imasdsf1olem  24356  isxms  24430  xmspropd  24456  imasf1oxms  24472  stdbdmopn  24501  isngp3  24581  ngppropd  24620  tngngp3  24639  isnlm  24658  nmvs  24659  xrsxmet  24793  cnheibor  24940  htpyi  24959  htpycc  24965  pi1xfr  25040  pi1coghm  25046  isclm  25049  lmhmclm  25072  isclmp  25082  clmmulg  25086  iscph  25155  tcphcph  25222  cphsscph  25236  cmetcaulem  25273  bcth3  25316  ovolunlem1a  25481  ovolicc2lem1  25502  ovolicc2lem4  25505  ovolicc2  25507  mblsplit  25517  volun  25530  volfiniun  25532  voliunlem1  25535  volsup  25541  ioorinv  25561  uniioombllem2  25568  vitalilem3  25595  mbfeqalem1  25626  mbflim  25653  itgeqa  25799  itgconst  25804  itgfsum  25812  itgsplitioo  25823  dvnadd  25914  dvnres  25916  dvexp  25938  dvmptfsum  25960  mvth  25977  dvlip  25978  lhop1lem  25998  dvcvx  26005  mdegle0  26060  ply1nzb  26106  mon1pval  26125  facth1  26150  ig1pval  26159  dgrmulc  26254  dgrcolem1  26256  dgrcolem2  26257  dgrco  26258  coecj  26261  coecjOLD  26263  vieta1lem2  26295  vieta1  26296  elqaalem3  26305  dvntaylp  26354  ulmss  26380  mtest  26387  sineq0  26506  efif1olem4  26527  cxpexp  26650  mulcxplem  26666  mulcxp  26667  cxpmul2  26671  cxpeq  26739  affineequiv2  26806  quad2  26821  dcubic  26828  leibpi  26924  o1cxp  26956  scvxcvx  26967  facgam  27047  wilthlem1  27049  wilthlem2  27050  mpodvdsmulf1o  27175  fsumdvdsmul  27176  perfect  27212  dchrelbas2  27218  dchrinv  27242  dchrptlem2  27246  lgsne0  27316  lgsqrlem2  27328  lgsdchr  27336  gausslemma2d  27355  lgseisenlem2  27357  lgsquad2lem2  27366  2lgslem1a  27372  2lgslem1b  27373  dchrisumlem1  27470  qabvexp  27607  ostthlem1  27608  ostthlem2  27609  ostth3  27619  ltsval2  27638  ltsres  27644  nolesgn2ores  27654  nogesgn1ores  27656  nolt02o  27677  nogt01o  27678  nosupcbv  27684  nosupno  27685  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  noinfcbv  27699  noinfno  27700  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem3  27707  noinfbnd1lem5  27709  addsrid  27974  addscom  27976  addscan1  28004  addsass  28015  subscan1d  28113  subscan2d  28114  mulsrid  28123  mulscom  28149  addsdilem3  28163  addsdilem4  28164  addsdi  28165  mulsasslem3  28175  mulsass  28176  mulscan2d  28189  mulscan1d  28190  bdayons  28286  om2noseqrdg  28314  n0cut  28344  expadds  28445  pw2cut  28470  pw2cut2  28472  elreno  28501  istrkgc  28540  istrkgcb  28542  istrkgld  28545  istrkg2ld  28546  axtgcgrrflx  28548  axtgupdim2  28557  tgjustf  28559  tgjustr  28560  iscgrg  28598  iscgrglt  28600  trgcgrg  28601  tgcgr4  28617  motcgr  28622  legso  28685  mirval  28741  israg  28783  ismidb  28864  isinagd  28925  f1otrgds  28955  ttgval  28961  ttgitvval  28968  brcgr  28987  brbtwn2  28992  colinearalglem1  28993  colinearalg  28997  ax5seglem1  29015  ax5seglem2  29016  ax5seglem8  29023  ax5seglem9  29024  axlowdimlem13  29041  axlowdimlem16  29044  axlowdim1  29046  axcontlem1  29051  axcontlem2  29052  axcontlem6  29056  axcontlem7  29057  axcontlem8  29058  ecgrtg  29070  usgredg2v  29314  issubgr  29358  cplgruvtxb  29500  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  32649  fmptcof2  32749  receqid  32836  bcm1n  32887  fsumiunle  32921  sgnsgn  32933  xmulcand  32999  xrsmulgzz  33088  psgnfzto1st  33186  isfxp  33249  fxpgaeq  33250  isslmd  33283  slmdlema  33284  gsumvsca1  33307  gsumvsca2  33308  urpropd  33312  elrgspnsubrunlem2  33329  erlval  33339  domnpropd  33358  domnlcanOLD  33361  qusvscpbl  33434  nsgqusf1olem3  33498  opprqusdrng  33576  ressply1mon1p  33651  ressply1invg  33652  deg1prod  33666  ply1moneq  33671  psrgsum  33732  psrmonmul  33734  psrmonprod  33736  vietalem  33763  vieta  33764  fedgmul  33815  brfldext  33829  fldextrspunlsplem  33857  extdgfialglem1  33876  bralgext  33881  minplyval  33889  submateq  33993  dispcmp  34043  pstmxmet  34081  cnre2csqlem  34094  mndpluscn  34110  qqhval2  34166  isrrext  34184  esumfzf  34253  esumcvg  34270  esum2dlem  34276  esumiun  34278  ofcfeqd2  34285  ismeas  34383  isrnmeas  34384  measvun  34393  carsgval  34487  inelcarsg  34495  carsgclctunlem1  34501  carsgclctunlem2  34503  pmeasmono  34508  pmeasadd  34509  eulerpartlemgvv  34560  eulerpartlemn  34565  sseqp1  34579  probun  34603  breprexp  34817  istrkg2d  34850  axtgupdim2ALTV  34852  afsval  34855  bnj1385  35014  bnj66  35042  bnj106  35050  bnj155  35061  bnj222  35065  bnj540  35074  bnj591  35093  bnj594  35094  bnj611  35100  bnj893  35110  bnj1000  35123  bnj966  35126  bnj1112  35165  bnj1234  35195  bnj1253  35199  bnj1280  35202  bnj1326  35208  bnj1450  35232  bnj1463  35237  bnj1529  35252  f1resveqaeq  35266  pfxwlk  35352  revwlk  35353  subfacp1lem3  35410  subfacp1lem4  35411  subfacp1lem5  35412  subfacp1lem6  35413  subfacval2  35415  erdszelem9  35427  sconnpht  35457  ptpconn  35461  cvmliftmolem1  35509  cvmliftmolem2  35510  cvmliftlem10  35522  cvmlift2  35544  cvmliftphtlem  35545  satfdm  35597  gonarlem  35622  gonar  35623  goalr  35625  satfdmfmla  35628  prv  35656  mrsubff1  35742  mrsubccat  35746  elmrsubrn  35748  mrsubvrs  35750  elmpst  35764  msrid  35773  msubvrs  35788  sqdivzi  35956  shftvalg  35960  bcprod  35966  bccolsum  35967  iprodefisumlem  35968  faclimlem1  35971  rdgprc  36020  dfrdg2  36021  elwlim  36049  fvsingle  36146  fullfunfv  36175  lineelsb2  36376  rankung  36394  ranksng  36395  rankpwg  36397  opnregcld  36558  cldregopn  36559  neibastop3  36590  weiunval  36690  csbttc  36737  mh-inf3f1  36769  bj-sbeqALT  37253  bj-gabeqis  37291  bj-isclm  37651  rdgeqoa  37732  fvineqsnf1  37772  tan2h  37979  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem9  37996  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem19  38006  broucube  38021  voliunnfl  38031  volsupnfl  38032  cocanfo  38086  upixp  38096  sdclem2  38109  caushft  38128  ismtycnv  38169  ismtyima  38170  ismtybndlem  38173  ismtyres  38175  bfplem2  38190  bfp  38191  isass  38213  opidonOLD  38219  exidu1  38223  cmpidelt  38226  grpoeqdivid  38248  elghomlem2OLD  38253  ghomlinOLD  38255  ghomco  38258  isrngo  38264  rngoid  38269  rngoideu  38270  rngodi  38271  rngodir  38272  rngoass  38273  rngohomval  38331  isrngohom  38332  rngohomadd  38336  rngohommul  38337  iscom2  38362  iscringd  38365  crngocom  38368  crngohomfo  38373  dmncan2  38444  elsymrels4  39006  brredunds  39077  lshpset  39470  lcvexchlem4  39529  lcvexchlem5  39530  lflset  39551  islfl  39552  lfli  39553  islfld  39554  eqlkr3  39593  isopos  39672  oposlem  39674  opcon3b  39688  cmtvalN  39703  omllaw  39735  cvlexchb2  39823  cvlatexchb2  39827  cvlsupr2  39835  4atlem9  40095  4atlem10a  40096  4atlem11a  40099  4atlem12a  40102  4at2  40106  pmapglb2N  40263  pmapglb2xN  40264  paddasslem17  40328  ispsubclN  40429  ispsubcl2N  40439  lhpmod2i2  40530  lhpmod6i1  40531  4atexlemex2  40563  4atex  40568  4atex2-0aOLDN  40570  4atex2-0cOLDN  40572  ldilval  40605  ltrnfset  40609  ltrnset  40610  isltrn  40611  ltrneq2  40640  trnfsetN  40647  trnsetN  40648  istrnN  40649  cdlemd5  40694  cdleme0moN  40717  cdleme0nex  40782  cdleme18d  40787  cdleme31so  40871  cdleme31fv  40882  cdlemg2jlemOLDN  41085  cdlemg2fvlem  41086  cdlemg2klem  41087  istendo  41252  tendovalco  41257  tendoeq2  41266  dicelvalN  41670  dihval  41724  dihcnv11  41767  dihmeetlem13N  41811  dihlspsnat  41825  dochn0nv  41867  dochkrshp4  41881  lpolsetN  41974  lpolsatN  41980  lpolpolsatN  41981  lcfl1lem  41983  lclkrlem2a  41999  lclkrlem2e  42003  lcfls1lem  42026  lclkrs2  42032  lcdfval  42080  lcdval  42081  mapdffval  42118  mapdfval  42119  mapd0  42157  mapdpglem30  42194  mapdhval  42216  mapdheq2  42221  hdmap1vallem  42289  hdmap1val  42290  hdmap1cbv  42294  hdmapval3N  42330  hdmap10  42332  hdmapeq0  42336  hdmap14lem12  42371  hdmap14lem13  42372  hgmapfval  42378  hgmapvs  42383  hgmapvv  42418  hlhilocv  42449  recbothd  42477  lcmineqlem13  42526  isprimroot  42578  primrootsunit1  42582  aks6d1c1p1  42592  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  evl1gprodd  42602  aks6d1c1rh  42610  aks6d1c2lem3  42611  deg1gprod  42625  deg1pow  42626  sticksstones22  42653  aks6d1c6lem2  42656  aks5lem3a  42674  unitscyglem2  42681  unitscyglem3  42682  unitscyglem4  42683  ccatcan2d  42735  remulcan2d  42740  sumcubes  42790  expeqidd  42802  cxp112d  42818  cxp111d  42819  log11d  42823  sn-addcand  42897  sn-addcan2d  42899  sn-mullid  42913  nn0addcom  42952  renegmulnnass  42955  nn0mulcom  42956  zmulcomlem  42957  cnreeu  42980  abvexp  43018  fiabv  43022  prjsprel  43054  prjcrvfval  43081  flt0  43087  sn-isghm  43123  ismrcd2  43148  ismrc  43150  dvdsrabdioph  43255  fphpdo  43262  rmxypairf1o  43356  monotoddzzfi  43387  monotoddzz  43388  oddcomabszz  43389  rmxdioph  43461  expdiophlem2  43467  dnnumch3  43492  aomclem8  43506  islssfg  43515  unxpwdom3  43540  gicabl  43544  idomodle  43636  fgraphxp  43649  hausgraph  43650  onov0suclim  43719  oaabsb  43739  oaomoencom  43762  oenass  43764  omabs2  43777  tfsconcat0b  43791  nadd1suc  43837  naddonnn  43840  minregex  43978  relexpmulnn  44153  clsk1independent  44490  ntrclsk13  44515  ntrclsk4  44516  imo72b2  44616  grumnud  44730  nzss  44761  caofcan  44767  expgrowth  44779  fperiodmullem  45751  uzinico3  46007  fsumf1of  46019  fmuldfeq  46028  fprodexp  46039  fprodabs2  46040  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climaddf  46060  mullimc  46061  limcperiod  46073  neglimc  46090  addlimc  46091  0ellimcdiv  46092  climeldmeqmpt  46111  climfveqmpt  46114  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  climeqf  46131  climeldmeqmpt3  46132  limsupequz  46166  cncfperiod  46322  icccncfext  46330  fperdvper  46362  dvnmptdivc  46381  dvnxpaek  46385  dvnmul  46386  dvmptfprod  46388  dvnprodlem3  46391  itgspltprt  46422  stoweidlem30  46473  stoweidlem48  46491  wallispilem4  46511  wallispi2lem1  46514  wallispi2lem2  46515  fourierdlem50  46599  fourierdlem73  46622  fourierdlem81  46630  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem92  46641  fourierdlem94  46643  fourierdlem97  46646  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  sge0iunmptlemfi  46856  ismea  46894  meadjuni  46900  meaiuninclem  46923  caragenval  46936  isome  46937  caragensplit  46943  carageniuncllem1  46964  caratheodorylem1  46969  hoidmvlelem3  47040  vonvolmbllem  47103  vonvolmbl  47104  smflimlem3  47216  smflim  47220  smfpimcc  47251  smfsuplem2  47255  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