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 567	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  neeq12d  3006  cdeqeq  3711  sbceqg  4344  csbun  4373  csbin  4374  csbdif  4459  csbif  4517  uniprgOLD  4860  intprgOLD  4916  iununi  5029  csbopab  5469  csbopabgALT  5470  dfid2  5492  csbima12  5990  dmsnsnsn  6128  csbcog  6204  dfpred3g  6218  preddowncl  6239  limeq  6282  csbiota  6430  fveqres  6825  opabiota  6860  fvmptf  6905  eqfnfv2f  6922  fvreseq0  6924  fveqdmss  6965  fvcofneq  6978  fnressn  7039  fnelfp  7056  fprb  7078  fnprb  7093  fntpb  7094  f1cofveqaeqALT  7141  nvocnv  7162  cocan1  7172  cocan2  7173  2fvcoidd  7178  fliftfun  7192  weniso  7234  csbriota  7257  oveqrspc2v  7311  csbov123  7326  eqfnov  7412  ovmpos  7430  ov2gf  7431  ovmpodxf  7432  caovcomg  7476  caovassg  7479  caovcang  7482  caovcanrd  7484  caovcan  7485  caovdig  7495  caovdirg  7498  caovmo  7518  offveqb  7567  caofid0l  7573  caofid0r  7574  caofass  7579  caonncan  7583  ordunisuc  7688  onsucuni2  7690  orduninsuc  7699  op1stg  7852  op2ndg  7853  f1o2ndf1  7972  fnsuppres  8016  csbfrecsg  8109  fpr3g  8110  frrlem1  8111  frrlem12  8122  frrlem13  8123  fpr2a  8127  wfr3g  8147  wfrlem1OLD  8148  wfrlem3OLDa  8151  wfrlem12OLD  8160  wfrlem14OLD  8162  wfrlem15OLD  8163  wfr2aOLD  8166  onfununi  8181  tfrlem1  8216  tfrlem3a  8217  tfrlem5  8220  tfrlem9  8225  tfrlem11  8228  tfrlem12  8229  tfr3  8239  tz7.44-1  8246  tz7.44-2  8247  tz7.44-3  8248  rdglem1  8255  rdg0g  8267  seqomlem1  8290  oalim  8371  omlim  8372  oelim  8373  oa0r  8377  om0r  8378  om1r  8383  oaass  8401  oarec  8402  odi  8419  omass  8420  oelim2  8435  oeoalem  8436  oeoa  8437  oeoelem  8438  oeoe  8439  nna0r  8449  nnacom  8457  nnaass  8462  nndi  8463  nnmass  8464  nnmsucr  8465  nnmcom  8466  oaabs  8487  oaabs2  8488  omabs  8490  ecovcom  8621  ecovass  8622  ecovdi  8623  dom2lem  8789  unxpdomlem2  9037  unxpdomlem3  9038  ixpfi2  9126  fipreima  9134  ordiso2  9283  wemaplem1  9314  wemaplem2  9315  wemapsolem  9318  cantnfval2  9436  cantnfp1lem3  9447  oemapvali  9451  cantnflem1c  9454  cantnflem1  9456  wemapwe  9464  rnttrcl  9489  tcvalg  9505  frr3g  9523  frr2  9527  rankvalg  9584  rankonidlem  9595  ranklim  9611  rankuni  9630  updjud  9701  cardprclem  9746  cardprc  9747  carduni  9748  fseqenlem1  9789  fodomacn  9821  alephcard  9835  alephfp2  9874  alephval3  9875  dfac12lem1  9908  dfac12lem2  9909  dfac12r  9911  ackbij1lem8  9992  ackbij1lem14  9998  ackbij1lem16  10000  ackbij2lem3  10006  cardcf  10017  sornom  10042  fin23lem28  10105  isf32lem2  10119  itunitc  10186  ituniiun  10187  axdc3lem2  10216  axdc4lem  10220  ttukeylem3  10276  ttukey2g  10281  fpwwe2lem7  10402  fpwwecbv  10409  canth4  10412  pwfseqlem2  10424  addcanpi  10664  mulcanpi  10665  recrecnq  10732  ltexnq  10740  genpv  10764  0idsr  10862  1idsr  10863  ax1rid  10926  mulid1  10982  addcan  11168  addcan2  11169  mulcand  11617  mulcan2d  11618  mulcan2g  11638  div11  11670  divmuleq  11689  conjmul  11701  eqneg  11704  ofsubeq0  11979  rpnnen1lem6  12731  cnref1o  12734  xmulasslem  13028  xmulass  13030  xadddi2  13040  prunioo  13222  fzsuc2  13323  fzprval  13326  fztpval  13327  fzosplitprm1  13506  modadd1  13637  modmul1  13653  addmodlteq  13675  om2uzsuci  13677  om2uzrdg  13685  uzrdgxfr  13696  seq1  13743  seqp1  13745  seqfveq2  13754  seqfveq  13756  seqshft2  13758  seqsplit  13765  seqcaopr3  13767  seqcaopr2  13768  seqf1olem2a  13770  seqf1olem2  13772  seqf1o  13773  seqid  13777  seqid2  13778  seqhomo  13779  ser1const  13788  seqof2  13790  mulexp  13831  expadd  13834  expmul  13837  binom2  13942  sq01  13949  modexp  13962  bcpasc  14044  hashgadd  14101  hashdom  14103  hashfzo  14153  hashfzp1  14155  hashxplem  14157  hashxp  14158  hashmap  14159  hashpw  14160  hashbclem  14173  hashbc  14174  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  hashf1lem2  14179  hashf1  14180  seqcoll  14187  eqs1  14326  swrdspsleq  14387  pfxeq  14418  pfxsuff1eqwrdeq  14421  ccatopth2  14439  cats1un  14443  swrdccatin1  14447  swrdccat3blem  14461  cshf1  14532  repswcshw  14534  s2eq2s1eq  14658  s3eqs2s1eq  14660  pfx2  14669  2swrd2eqwrdeq  14675  wwlktovf1  14681  eqwrds3  14685  relexpsucnnr  14745  relexpsucnnl  14750  relexpcnv  14755  relexpaddnn  14771  replim  14836  cjreb  14843  cjexp  14870  absexp  15025  abs1m  15056  recan  15057  cnsqrt00  15113  isercoll2  15389  iseraltlem2  15403  iseraltlem3  15404  sumeq2ii  15414  zsum  15439  fsum  15441  fsumf1o  15444  sumss  15445  fsumcvg2  15448  fsumadd  15461  isummulc2  15483  fsum2d  15492  fsummulc2  15505  fsumconst  15511  modfsummods  15514  modfsummod  15515  fsumparts  15527  fsumrelem  15528  fsumiun  15542  binom  15551  bcxmas  15556  incexclem  15557  isumshft  15560  isumnn0nn  15563  climcndslem1  15570  climcndslem2  15571  mertenslem2  15606  clim2prod  15609  prodfrec  15616  prodeq2ii  15632  zprod  15656  fprod  15660  fprodf1o  15665  fprodser  15668  fprodmul  15679  fproddiv  15680  prodsn  15681  prodsnf  15683  fprodabs  15693  fprodconst  15697  fprod2d  15700  fprodmodd  15716  binomfallfac  15760  bpolydif  15774  fprodefsum  15813  efne0  15815  efexp  15819  demoivreALT  15919  moddvds  15983  bitsinv1  16158  sadadd2  16176  smu01lem  16201  smupval  16204  smueqlem  16206  smumullem  16208  gcdaddm  16241  bezoutlem1  16256  bezout  16260  gcddiv  16268  seq1st  16285  alginv  16289  algfx  16294  lcmneg  16317  lcmid  16323  lcmgcdeq  16326  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfunsnlem  16355  lcmfunsn  16358  lcmfun  16359  divgcdcoprm0  16379  cncongr1  16381  cncongr2  16382  nn0gcdsq  16465  crth  16488  eulerthlem2  16492  pythagtriplem1  16526  iserodd  16545  pcqmul  16563  pcexp  16569  pcneg  16584  pcmpt  16602  pcfac  16609  prmreclem2  16627  prmreclem3  16628  1arith  16637  vdwpc  16690  ramcl  16739  prmop1  16748  imasval  17231  ercpbllem  17268  iscat  17390  iscatd  17391  catideu  17393  iscatd2  17399  catlid  17401  catrid  17402  catass  17404  homfeq  17412  comfeq  17424  catpropd  17427  moni  17457  epii  17464  sectffval  17471  sectfval  17472  oppcsect  17499  sectmon  17503  isfunc  17588  funcid  17594  funcco  17595  funcpropd  17625  isfull  17635  fthsect  17650  fthmon  17652  natfval  17671  isnat  17672  nati  17680  fucsect  17699  natpropd  17703  setcmon  17811  setcepi  17812  setcsect  17813  fthestrcsetc  17876  embedsetcestrclem  17883  fthsetcestrc  17891  evlfcl  17949  uncfcurf  17966  yoniso  18012  joinval  18104  meetval  18118  islat  18160  latdisdlem  18223  latdisd  18224  isclat  18227  isdlat  18249  dlatmjdi  18250  isacs5lem  18272  acsdrscl  18273  acsficl  18274  isps  18295  mgmidmo  18353  mgmlrid  18360  lidrideqd  18362  lidrididd  18363  grprinvlem  18366  grprinvd  18367  gsumvalx  18369  gsumval2  18379  issgrp  18385  isnsgrp  18388  sgrpass  18390  sgrp1  18393  ismndd  18416  mndpropd  18419  imasmnd2  18431  mnd1  18435  mnd1id  18436  ismhm  18441  mhmpropd  18445  mhmlin  18446  mhmeql  18473  gsumccatOLD  18488  gsumccat  18489  gsumwmhm  18493  frmdgsum  18510  symggrplem  18532  smndex1mndlem  18557  smndex1n0mnd  18560  sgrp2rid2  18574  sgrp2nmndlem4  18576  isgrp  18592  grppropd  18603  isgrpd2e  18607  dfgrp2  18613  isgrpid2  18625  grpidd2  18626  grpinvfval  18627  grpinvfvalALT  18628  grpinvpropd  18659  grpidssd  18660  grpinvssd  18661  grpsubrcan  18665  dfgrp3lem  18682  grplactcnv  18687  imasgrp2  18699  mhmlem  18704  mulgnn0p1  18724  mulgaddcom  18736  mulginvcom  18737  mulgneg2  18746  mulgnnass  18747  mulgnn0ass  18748  mulgass  18749  mhmmulg  18753  cyccom  18831  isghm  18843  ghmlin  18848  ghmeql  18866  isga  18906  gagrpid  18909  gaass  18912  galcan  18919  orbsta  18928  cntzfval  18935  elcntz  18937  cntzsnval  18939  elcntzsn  18940  cntzi  18944  resscntz  18947  cntzmhm  18954  gsumwrev  18982  snsymgefmndeq  19011  cayleylem2  19030  symgextf1  19038  gsmsymgreqlem2  19048  gsmsymgreq  19049  symgfixf1  19054  pmtrfrn  19075  odfval  19149  odfvalALT  19150  mndodcong  19159  odbezout  19174  odeq1  19176  submod  19183  gexval  19192  gexdvds  19198  ispgp  19206  sylow1lem1  19212  sylow2alem1  19231  sylow2alem2  19232  sylow2blem2  19235  efgmnvl  19329  efgredlemc  19360  efgredeu  19367  frgpuptinv  19386  frgpup1  19390  frgpup3lem  19392  iscmn  19403  cmnpropd  19405  iscmnd  19408  abladdsub4  19424  submcmn2  19449  qusabl  19475  abl1  19476  iscyg  19488  cycsubmcmn  19498  cygablOLD  19501  gsum2dlem2  19581  telgsumfzs  19599  dmdprd  19610  dprdval  19615  dprdfcntz  19627  subgdmdprd  19646  dprd2da  19654  dpjrid  19674  pgpfac1lem3a  19688  ablfaclem3  19699  ablfac2  19701  issrg  19752  srgmulgass  19776  srgpcomp  19777  srgbinom  19790  isring  19796  ringpropd  19830  ringinvnz1ne0  19840  mulgass2  19849  ring1  19850  imasring  19867  dvdsr  19897  dvreq1  19944  isdrng  20004  drngprop  20011  isdrngd  20025  drngpropd  20027  cntzsdrg  20079  isabv  20088  abvmul  20098  issrng  20119  issrngd  20130  idsrngd  20131  islmod  20136  lmodlema  20137  islmodd  20138  lmodvsmmulgdi  20167  lmodprop2d  20194  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  islmhm  20298  lmhmlin  20306  islmhm2  20309  lmhmeql  20326  lmhmpropd  20344  islbs  20347  lbspropd  20370  quscrng  20520  islpir  20529  rrgval  20567  unitrrg  20573  cnfldmulg  20639  cnfldexp  20640  prmirredlem  20703  chrcong  20742  zndvds  20766  znf1o  20768  znunit  20780  cygznlem3  20786  frgpcyg  20790  psgndiflemB  20814  isphl  20842  ipcj  20848  iporthcom  20849  ip2eq  20867  isphld  20868  phlpropd  20869  phlssphl  20873  ocvfval  20880  iscss  20897  ishil  20934  isobs  20936  obsip  20937  obslbs  20946  frlmphl  20997  isassa  21072  assalem  21073  isassad  21080  assapropd  21085  assamulgscm  21114  mvrf1  21203  mplmonmul  21246  mplcoe1  21247  mplcoe3  21248  mplcoe5lem  21249  mplcoe5  21250  evlslem1  21301  mpfrcl  21304  evlsval  21305  coe1tm  21453  ply1sclf1  21469  ply1coe  21476  eqcoe1ply1eq  21477  cply1coe0bi  21480  coe1fzgsumd  21482  gsumply1eq  21485  evl1gsumd  21532  mat0dimcrng  21628  mat1ghm  21641  mat1mhm  21642  dmatcrng  21660  scmateALT  21670  scmatcrng  21679  scmatf1  21689  mvmumamul1  21712  mdetdiagid  21758  mdetralt  21766  mdetunilem1  21770  mdetunilem3  21772  mdetunilem4  21773  mdetunilem7  21776  mdetunilem9  21778  mdetuni0  21779  madugsum  21801  smadiadetr  21833  mat2pmatf1  21887  m2cpminvid2lem  21912  decpmataa0  21926  pmatcollpw2lem  21935  pm2mpf1  21957  chcoeffeqlem  22043  chcoeffeq  22044  cayhamlem3  22045  cayleyhamilton1  22050  isperf  22311  restperf  22344  cmpsub  22560  isconn  22573  2ndcsep  22619  elptr2  22734  ptbasin  22737  dfac14  22778  txcnp  22780  ptcnplem  22781  ptcnp  22782  cnmpt11  22823  cnmpt21  22831  cnmptcom  22838  kqfeq  22884  isr0  22897  pt1hmeo  22966  ustexsym  23376  isusp  23422  imasdsf1olem  23535  isxms  23609  xmspropd  23635  imasf1oxms  23654  stdbdmopn  23683  isngp3  23763  ngppropd  23802  tngngp3  23829  isnlm  23848  nmvs  23849  xrsxmet  23981  cnheibor  24127  htpyi  24146  htpycc  24152  pi1xfr  24227  pi1coghm  24233  isclm  24236  lmhmclm  24259  isclmp  24269  clmmulg  24273  iscph  24343  tcphcph  24410  cphsscph  24424  cmetcaulem  24461  bcth3  24504  ovolunlem1a  24669  ovolicc2lem1  24690  ovolicc2lem4  24693  ovolicc2  24695  mblsplit  24705  volun  24718  volfiniun  24720  voliunlem1  24723  volsup  24729  ioorinv  24749  uniioombllem2  24756  vitalilem3  24783  mbfeqalem1  24814  mbflim  24841  itgeqa  24987  itgconst  24992  itgfsum  25000  itgsplitioo  25011  dvnadd  25102  dvnres  25104  dvexp  25126  dvmptfsum  25148  mvth  25165  dvlip  25166  lhop1lem  25186  dvcvx  25193  mdegle0  25251  ply1nzb  25296  mon1pval  25315  facth1  25338  ig1pval  25346  dgrmulc  25441  dgrcolem1  25443  dgrcolem2  25444  dgrco  25445  coecj  25448  vieta1lem2  25480  vieta1  25481  elqaalem3  25490  dvntaylp  25539  ulmss  25565  mtest  25572  sineq0  25689  efif1olem4  25710  cxpexp  25832  mulcxplem  25848  mulcxp  25849  cxpmul2  25853  cxpeq  25919  affineequiv2  25983  quad2  25998  dcubic  26005  leibpi  26101  o1cxp  26133  scvxcvx  26144  facgam  26224  wilthlem1  26226  wilthlem2  26227  perfect  26388  dchrelbas2  26394  dchrinv  26418  dchrptlem2  26422  lgsne0  26492  lgsqrlem2  26504  lgsdchr  26512  gausslemma2d  26531  lgseisenlem2  26533  lgsquad2lem2  26542  2lgslem1a  26548  2lgslem1b  26549  dchrisumlem1  26646  qabvexp  26783  ostthlem1  26784  ostthlem2  26785  ostth3  26795  istrkgc  26824  istrkgcb  26826  istrkgld  26829  istrkg2ld  26830  axtgcgrrflx  26832  axtgupdim2  26841  tgjustf  26843  tgjustr  26844  iscgrg  26882  iscgrglt  26884  trgcgrg  26885  tgcgr4  26901  motcgr  26906  legso  26969  mirval  27025  israg  27067  ismidb  27148  isinagd  27209  f1otrgds  27239  ttgval  27245  ttgvalOLD  27246  ttgitvval  27258  brcgr  27277  brbtwn2  27282  colinearalglem1  27283  colinearalg  27287  ax5seglem1  27305  ax5seglem2  27306  ax5seglem8  27313  ax5seglem9  27314  axlowdimlem13  27331  axlowdimlem16  27334  axlowdim1  27336  axcontlem1  27341  axcontlem2  27342  axcontlem6  27346  axcontlem7  27347  axcontlem8  27348  ecgrtg  27360  usgredg2v  27603  issubgr  27647  cplgruvtxb  27789  cusgrsize  27830  finsumvtxdg2size  27926  isrgr  27935  wkslem1  27983  wkslem2  27984  iswlk  27986  uspgr2wlkeq  28022  2wlklem  28044  wlkres  28047  redwlk  28049  wlkp1lem6  28055  wlkp1lem7  28056  wlkp1lem8  28057  pthdivtx  28106  upgrwlkdvdelem  28113  isclwlk  28150  iscrct  28167  iscycl  28168  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  wwlksnextinj  28273  rusgrnumwwlk  28349  clwlkclwwlklem2  28373  clwlkclwwlkf1lem3  28379  clwlkclwwlkf1  28383  erclwwlkeq  28391  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  erclwwlkneq  28440  clwwlkvbij  28486  upgreupthseg  28582  eupth2eucrct  28590  eupth2lem3  28609  eupth2  28612  eucrctshift  28616  2clwwlk  28720  numclwwlk1lem2f1  28730  numclwlk1lem1  28742  numclwlk1lem2  28743  numclwlk2lem2f1o  28752  isgrpo  28868  grpoass  28874  grpoidinvlem3  28877  grpoidinv  28879  grpoideu  28880  grpoidinv2  28886  grpoinvfval  28893  isablo  28917  ablocom  28919  vciOLD  28932  vcidOLD  28935  vcdi  28936  vcdir  28937  vcass  28938  isvclem  28948  isnvlem  28981  nvmeq0  29029  nvs  29034  imsmetlem  29061  islno  29124  lnolin  29125  ishmo  29182  isphg  29188  phpar2  29194  phpar  29195  ipdiri  29201  ipasslem1  29202  ipasslem5  29206  ipasslem11  29211  ipassi  29212  dipdir  29213  dipass  29216  ip2eqi  29227  htth  29289  hvsubsub4  29431  hvnegdi  29438  hvaddcan  29441  hvaddcan2  29442  hvsubcan  29445  hvsubcan2  29446  hvaddsub4  29449  hial2eq  29477  normlem9at  29492  normsq  29505  norm-iii  29511  normsub  29514  normpyth  29516  normpar  29526  polid  29530  issubgoilem  29631  ococ  29777  chj0  29868  chlejb1  29883  chdmm1  29896  chjass  29904  spanun  29916  spansn  29930  elspansn2  29938  cmbr  29955  cmbr3  29979  pjoml2  29982  pjoml3  29983  osum  30016  spansnj  30018  pjch1  30041  pjadji  30056  pjaddi  30057  pjinormi  30058  pjsubi  30059  pjmuli  30060  pjcjt2  30063  pjch  30065  pjopyth  30091  pjpyth  30096  hoaddcom  30145  hoaddass  30153  hocsubdir  30156  hoaddid1  30162  ho0sub  30168  honegsub  30170  adjsym  30204  eigrei  30205  eigre  30206  eigposi  30207  eigorth  30209  ellnop  30229  elhmop  30244  ellnfn  30254  cnvadj  30263  lnopl  30285  unop  30286  hmop  30293  lnfnl  30302  adj1  30304  eleigvec  30328  hoddi  30361  lnopeq0lem2  30377  lnopunilem1  30381  lnopunilem2  30382  lnopunii  30383  elunop2  30384  lnophmi  30389  lnfnmul  30419  cnlnadjlem5  30442  branmfn  30476  bra11  30479  hmopidmchi  30522  hmopidmch  30524  hmopidmpj  30525  pjss2coi  30535  pjssmi  30536  pjssge0i  30537  pjidmco  30552  dfpjop  30553  elpjrn  30561  isst  30584  ishst  30585  hstel2  30590  stj  30606  mdbr  30665  mdi  30666  mdbr3  30668  dmdbr  30670  dmdmd  30671  dmdi  30673  dmdbr3  30676  mddmd2  30680  mdsl1i  30692  chjatom  30728  iuninc  30909  fmptcof2  31003  bcm1n  31125  fsumiunle  31152  xmulcand  31204  xrsmulgzz  31296  gsumle  31359  psgnfzto1st  31381  isslmd  31464  slmdlema  31465  gsumvsca1  31488  gsumvsca2  31489  rngurd  31491  qusvscpbl  31560  nsgqusf1olem3  31609  ply1scleq  31677  ply1chr  31678  fedgmul  31721  brfldext  31731  submateq  31768  dispcmp  31818  pstmxmet  31856  cnre2csqlem  31869  mndpluscn  31885  qqhval2  31941  isrrext  31959  esumfzf  32046  esumcvg  32063  esum2dlem  32069  esumiun  32071  ofcfeqd2  32078  ismeas  32176  isrnmeas  32177  measvun  32186  carsgval  32279  inelcarsg  32287  carsgclctunlem1  32293  carsgclctunlem2  32295  pmeasmono  32300  pmeasadd  32301  eulerpartlemgvv  32352  eulerpartlemn  32357  sseqp1  32371  probun  32395  sgnsgn  32524  breprexp  32622  istrkg2d  32655  axtgupdim2ALTV  32657  afsval  32660  bnj1385  32821  bnj66  32849  bnj106  32857  bnj155  32868  bnj222  32872  bnj540  32881  bnj591  32900  bnj594  32901  bnj611  32907  bnj893  32917  bnj1000  32930  bnj966  32933  bnj1112  32972  bnj1234  33002  bnj1253  33006  bnj1280  33009  bnj1326  33015  bnj1450  33039  bnj1463  33044  bnj1529  33059  f1resveqaeq  33066  pfxwlk  33094  revwlk  33095  subfacp1lem3  33153  subfacp1lem4  33154  subfacp1lem5  33155  subfacp1lem6  33156  subfacval2  33158  erdszelem9  33170  sconnpht  33200  ptpconn  33204  cvmliftmolem1  33252  cvmliftmolem2  33253  cvmliftlem10  33265  cvmlift2  33287  cvmliftphtlem  33288  satfdm  33340  gonarlem  33365  gonar  33366  goalr  33368  satfdmfmla  33371  prv  33399  mrsubff1  33485  mrsubccat  33489  elmrsubrn  33491  mrsubvrs  33493  elmpst  33507  msrid  33516  msubvrs  33531  sqdivzi  33702  shftvalg  33706  bcprod  33713  bccolsum  33714  iprodefisumlem  33715  faclimlem1  33718  rdgprc  33779  dfrdg2  33780  xpord2pred  33801  xpord3pred  33807  poseq  33811  soseq  33812  elwlim  33826  naddcllem  33840  naddcom  33844  naddid1  33845  sltval2  33868  sltres  33874  nolesgn2ores  33884  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  nosupcbv  33914  nosupno  33915  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  noinfcbv  33929  noinfno  33930  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem3  33937  noinfbnd1lem5  33939  addsid1  34136  addscom  34138  fvsingle  34231  fullfunfv  34258  lineelsb2  34459  rankung  34477  ranksng  34478  rankpwg  34480  opnregcld  34528  cldregopn  34529  neibastop3  34560  bj-sbeqALT  35094  bj-gabeqis  35135  bj-isclm  35471  rdgeqoa  35550  fvineqsnf1  35590  tan2h  35778  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem9  35795  poimirlem13  35799  poimirlem14  35800  poimirlem16  35802  poimirlem19  35805  broucube  35820  voliunnfl  35830  volsupnfl  35831  cocanfo  35885  upixp  35896  sdclem2  35909  caushft  35928  ismtycnv  35969  ismtyima  35970  ismtybndlem  35973  ismtyres  35975  bfplem2  35990  bfp  35991  isass  36013  opidonOLD  36019  exidu1  36023  cmpidelt  36026  grpoeqdivid  36048  elghomlem2OLD  36053  ghomlinOLD  36055  ghomco  36058  isrngo  36064  rngoid  36069  rngoideu  36070  rngodi  36071  rngodir  36072  rngoass  36073  rngohomval  36131  isrngohom  36132  rngohomadd  36136  rngohommul  36137  iscom2  36162  iscringd  36165  crngocom  36168  crngohomfo  36173  dmncan2  36244  elsymrels4  36676  brredunds  36746  lshpset  36999  lcvexchlem4  37058  lcvexchlem5  37059  lflset  37080  islfl  37081  lfli  37082  islfld  37083  eqlkr3  37122  isopos  37201  oposlem  37203  opcon3b  37217  cmtvalN  37232  omllaw  37264  cvlexchb2  37352  cvlatexchb2  37356  cvlsupr2  37364  4atlem9  37624  4atlem10a  37625  4atlem11a  37628  4atlem12a  37631  4at2  37635  pmapglb2N  37792  pmapglb2xN  37793  paddasslem17  37857  ispsubclN  37958  ispsubcl2N  37968  lhpmod2i2  38059  lhpmod6i1  38060  4atexlemex2  38092  4atex  38097  4atex2-0aOLDN  38099  4atex2-0cOLDN  38101  ldilval  38134  ltrnfset  38138  ltrnset  38139  isltrn  38140  ltrneq2  38169  trnfsetN  38176  trnsetN  38177  istrnN  38178  cdlemd5  38223  cdleme0moN  38246  cdleme0nex  38311  cdleme18d  38316  cdleme31so  38400  cdleme31fv  38411  cdlemg2jlemOLDN  38614  cdlemg2fvlem  38615  cdlemg2klem  38616  istendo  38781  tendovalco  38786  tendoeq2  38795  dicelvalN  39199  dihval  39253  dihcnv11  39296  dihmeetlem13N  39340  dihlspsnat  39354  dochn0nv  39396  dochkrshp4  39410  lpolsetN  39503  lpolsatN  39509  lpolpolsatN  39510  lcfl1lem  39512  lclkrlem2a  39528  lclkrlem2e  39532  lcfls1lem  39555  lclkrs2  39561  lcdfval  39609  lcdval  39610  mapdffval  39647  mapdfval  39648  mapd0  39686  mapdpglem30  39723  mapdhval  39745  mapdheq2  39750  hdmap1vallem  39818  hdmap1val  39819  hdmap1cbv  39823  hdmapval3N  39859  hdmap10  39861  hdmapeq0  39865  hdmap14lem12  39900  hdmap14lem13  39901  hgmapfval  39907  hgmapvs  39912  hgmapvv  39947  hlhilocv  39982  recbothd  40008  lcmineqlem13  40056  sticksstones22  40131  ccatcan2d  40226  mhphf  40292  remulcan2d  40300  nnadd1com  40304  nnaddcom  40305  nnadddir  40307  nnmul1com  40308  nnmulcom  40309  sn-addcand  40408  sn-addcan2d  40410  sn-mulid2  40424  cnreeu  40445  prjsprel  40450  prjcrvfval  40475  flt0  40481  ismrcd2  40528  ismrc  40530  dvdsrabdioph  40639  fphpdo  40646  rmxypairf1o  40740  monotoddzzfi  40771  monotoddzz  40772  oddcomabszz  40773  rmxdioph  40845  expdiophlem2  40851  dnnumch3  40879  aomclem8  40893  islssfg  40902  unxpwdom3  40927  gicabl  40931  idomodle  41028  fgraphxp  41043  hausgraph  41044  minregex  41148  relexpmulnn  41324  clsk1independent  41663  ntrclsk13  41688  ntrclsk4  41689  imo72b2  41790  grumnud  41911  nzss  41942  caofcan  41948  expgrowth  41960  fsneq  42753  fperiodmullem  42849  uzinico3  43108  fsumf1of  43122  fmuldfeq  43131  fprodexp  43142  fprodabs2  43143  climmulf  43152  climexp  43153  climsuse  43156  climrecf  43157  climaddf  43163  mullimc  43164  limcperiod  43176  neglimc  43195  addlimc  43196  0ellimcdiv  43197  climeldmeqmpt  43216  climfveqmpt  43219  climfveqf  43228  climfveqmpt3  43230  climeldmeqf  43231  climeqf  43236  climeldmeqmpt3  43237  limsupequz  43271  cncfperiod  43427  icccncfext  43435  fperdvper  43467  dvnmptdivc  43486  dvnxpaek  43490  dvnmul  43491  dvmptfprod  43493  dvnprodlem3  43496  itgspltprt  43527  stoweidlem30  43578  stoweidlem48  43596  wallispilem4  43616  wallispi2lem1  43619  wallispi2lem2  43620  fourierdlem50  43704  fourierdlem73  43727  fourierdlem81  43735  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem94  43748  fourierdlem97  43751  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  sge0iunmptlemfi  43958  ismea  43996  meadjuni  44002  meaiuninclem  44025  caragenval  44038  isome  44039  caragensplit  44045  carageniuncllem1  44066  caratheodorylem1  44071  hoidmvlelem3  44142  vonvolmbllem  44205  vonvolmbl  44206  smflimlem3  44318  smflim  44322  smfpimcc  44352  smfsuplem2  44356  fsetsnf1  44557  cfsetsnfsetf1  44564  fcoresf1  44574  csbafv12g  44640  csbaovg  44683  csbafv212g  44722  fargshiftf1  44904  fargshiftfva  44906  prproropf1olem4  44969  fmtnorec2  45006  fmtnoprmfac1lem  45027  fmtnofac1  45033  quad1  45083  requad1  45085  perfectALTV  45186  fpprwppr  45202  nfermltl8rev  45205  nfermltl2rev  45206  nfermltlrev  45207  sbgoldbo  45250  isomgr  45286  isomushgr  45289  isomuspgrlem1  45290  isomuspgrlem2c  45293  isomuspgrlem2d  45294  isomuspgr  45297  isomgrsym  45299  isomgrtrlem  45301  uspgrsprf1  45320  plusfreseq  45337  ismgmhm  45348  mgmhmpropd  45350  mgmhmlin  45351  mgmhmeql  45368  iscomlaw  45395  isasslaw  45397  isrng  45445  rngdir  45451  rnghmval  45460  isrnghm  45461  rnghmmul  45469  c0snmgmhm  45483  zrrnghm  45486  lidldomn1  45490  lidlmsgrp  45495  lidlrng  45496  zlidlring  45497  rngcsect  45549  rngcsectALTV  45561  ringcsect  45600  ringcsectALTV  45624  ovmpordxf  45685  lmodvsmdi  45729  islininds  45798  lindslinindimp2lem4  45813  lindslinindsimp2  45815  lmod1  45844  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem1  45978  nn0sumshdig  45980  1arymaptf1  45999  2arymaptf1  46010  itcovalpc  46029  itcovalt2  46034  rrx2pnecoorneor  46072  rrx2plordisom  46080  rrx2line  46097  rrx2linest  46099  line2ylem  46108  line2x  46111  line2y  46112  itscnhlc0yqe  46116  itscnhlc0xyqsol  46122  idmon  46308  idepi  46309  grptcmon  46388  grptcepi  46389  aacllem  46516