Theorem eqeq12d 2779

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  neeq12d  3019  cdeqeq  3735  sbceqg  4372  csbun  4401  csbin  4402  csbdif  4483  csbif  4542  iununi  5061  csbopab  5533  csbopabw  5534  dfid2  5551  csbima12  6081  dmsnsnsn  6227  csbcog  6306  dfpred3g  6322  preddowncl  6341  limeq  6380  csbiota  6539  fveqres  6937  opabiota  6975  fvmptf  7023  eqfnfv2f  7041  fsneq  7042  fvreseq0  7045  fveqdmss  7086  fvcofneq  7101  fnressn  7170  fnelfp  7187  fprb  7206  fnprb  7221  fntpb  7222  f1cofveqaeqALT  7269  f1resveqaeq  7284  nvocnv  7296  cocan1  7306  cocan2  7307  2fvcoidd  7312  fliftfun  7327  weniso  7371  csbriota  7399  oveqrspc2v  7454  csbov123  7471  eqfnov  7556  ovmpos  7575  ov2gf  7576  ovmpodxf  7577  caovcomg  7623  caovassg  7626  caovcang  7629  caovcanrd  7631  caovcan  7632  caovdig  7642  caovdirg  7645  caovmo  7665  coof  7724  offveqb  7727  caofid0l  7733  caofid0r  7734  caofidlcan  7738  caofass  7740  caonncan  7744  onsucuni2  7852  orduninsuc  7861  op1stg  8020  op2ndg  8021  f1o2ndf1  8143  xpord2pred  8172  xpord3pred  8179  poseq  8185  soseq  8186  fnsuppres  8219  csbfrecsg  8313  fpr3g  8314  frrlem1  8315  frrlem12  8326  frrlem13  8327  fpr2a  8331  wfr3g  8348  onfununi  8360  tfrlem1  8394  tfrlem3a  8395  tfrlem5  8398  tfrlem9  8404  tfrlem11  8407  tfrlem12  8408  tfr3  8418  tz7.44-1  8425  tz7.44-2  8426  tz7.44-3  8427  rdglem1  8434  rdg0g  8446  seqomlem1  8471  oalim  8551  omlim  8552  oelim  8553  oa0r  8557  om0r  8558  om1r  8562  oaass  8580  oarec  8581  odi  8598  omass  8599  oelim2  8615  oeoalem  8616  oeoa  8617  oeoelem  8618  oeoe  8619  nna0r  8629  nnacom  8637  nnaass  8642  nndi  8643  nnmass  8644  nnmsucr  8645  nnmcom  8646  oaabs  8668  oaabs2  8669  omabs  8671  naddcllem  8696  naddcom  8703  naddrid  8704  naddass  8717  naddsuc2  8722  naddoa  8723  ecovcom  8855  ecovass  8856  ecovdi  8857  dom2lem  9030  unxpdomlem2  9259  unxpdomlem3  9260  ixpfi2  9350  fipreima  9358  ordiso2  9519  wemaplem1  9550  wemaplem2  9551  wemapsolem  9554  cantnfval2  9680  cantnfp1lem3  9691  oemapvali  9695  cantnflem1c  9698  cantnflem1  9700  wemapwe  9708  rnttrcl  9733  tcvalg  9747  frr3g  9770  frr2  9774  rankvalg  9836  rankonidlem  9848  rankpwg  9867  ranklim  9868  rankung  9883  ranksng  9884  rankuni  9889  updjud  10025  cardprclem  10070  cardprc  10071  carduni  10072  fseqenlem1  10113  fodomacn  10145  alephcard  10159  alephfp2  10198  alephval3  10199  dfac12lem1  10232  dfac12lem2  10233  dfac12r  10235  ackbij1lem8  10314  ackbij1lem14  10320  ackbij1lem16  10322  ackbij2lem3  10328  cardcf  10339  sornom  10365  fin23lem28  10428  isf32lem2  10442  itunitc  10509  ituniiun  10510  axdc3lem2  10539  axdc4lem  10543  ttukeylem3  10599  ttukey2g  10604  fpwwe2lem7  10732  fpwwecbv  10739  canth4  10742  pwfseqlem2  10754  addcanpi  10994  mulcanpi  10995  recrecnq  11062  ltexnq  11070  genpv  11094  0idsr  11192  1idsr  11193  ax1rid  11256  mulrid  11316  addcan  11504  addcan2  11505  mulcand  11959  mulcan2d  11960  mulcan2g  11980  divmuleq  12032  conjmul  12044  eqneg  12047  ofsubeq0  12327  nnadd1com  12371  nnaddcom  12372  nnadddir  12404  nnmul1com  12405  nnmulcom  12406  rpnnen1lem6  13120  cnref1o  13123  xmulasslem  13425  xmulass  13427  xadddi2  13437  prunioo  13622  fzsuc2  13726  fzprval  13729  fztpval  13730  fzosplitprm1  13923  modadd1  14058  modaddb  14059  modmul1  14077  addmodlteq  14099  om2uzsuci  14101  om2uzrdg  14109  uzrdgxfr  14120  seq1  14167  seqp1  14169  seqfveq2  14177  seqfveq  14179  seqshft2  14181  seqsplit  14188  seqcaopr3  14190  seqcaopr2  14191  seqf1olem2a  14193  seqf1olem2  14195  seqf1o  14196  seqid  14200  seqid2  14201  seqhomo  14202  ser1const  14211  seqof2  14213  mulexp  14254  expadd  14257  expmul  14260  binom2  14371  sq01  14379  modexp  14392  bcpasc  14475  hashgadd  14531  hashdom  14533  hashfzo  14584  hashfzp1  14586  hashxplem  14588  hashxp  14589  hashmap  14590  hashpw  14591  hashbclem  14607  hashbc  14608  hashfacen  14609  hashf1lem1  14610  hashf1lem2  14611  hashf1  14612  seqcoll  14619  eqs1  14771  swrdspsleq  14826  pfxeq  14856  pfxsuff1eqwrdeq  14859  ccatopth2  14877  cats1un  14881  swrdccatin1  14885  swrdccat3blem  14899  cshf1  14972  repswcshw  14974  s2eq2s1eq  15099  s3eqs2s1eq  15101  pfx2  15110  2swrd2eqwrdeq  15118  wwlktovf1  15122  eqwrds3  15126  relexpsucnnr  15190  relexpsucnnl  15195  relexpcnv  15200  relexpaddnn  15216  replim  15295  cjreb  15302  cjexp  15329  absexp  15483  abs1m  15515  recan  15516  cnsqrt00  15572  isercoll2  15848  iseraltlem2  15862  iseraltlem3  15863  sumeq2ii  15872  zsum  15896  fsum  15898  fsumf1o  15901  sumss  15902  fsumcvg2  15905  fsumadd  15918  isummulc2  15940  fsum2d  15949  fsummulc2  15962  fsumconst  15968  modfsummods  15972  modfsummod  15973  fsumparts  15985  fsumrelem  15986  fsumiun  16000  binom  16011  bcxmas  16016  incexclem  16017  isumshft  16020  isumnn0nn  16023  climcndslem1  16030  climcndslem2  16031  mertenslem2  16066  clim2prod  16069  prodfrec  16076  prodeq2ii  16092  zprod  16116  fprod  16120  fprodf1o  16125  fprodser  16128  fprodmul  16139  fproddiv  16140  prodsn  16141  prodsnf  16143  fprodabs  16153  fprodconst  16157  fprod2d  16160  fprodmodd  16176  binomfallfac  16219  bpolydif  16233  fprodefsum  16273  efne0d  16275  efne0OLD  16277  efexp  16281  demoivreALT  16381  moddvds  16445  bitsinv1  16624  sadadd2  16642  smu01lem  16667  smupval  16670  smueqlem  16672  smumullem  16674  gcdaddm  16709  bezoutlem1  16724  bezout  16728  gcddiv  16736  seq1st  16758  alginv  16762  algfx  16767  lcmneg  16790  lcmid  16796  lcmgcdeq  16799  lcmfunsnlem1  16824  lcmfunsnlem2lem1  16825  lcmfunsnlem2lem2  16826  lcmfunsnlem  16828  lcmfunsn  16831  lcmfun  16832  divgcdcoprm0  16852  cncongr1  16854  cncongr2  16855  nn0gcdsq  16940  crth  16967  eulerthlem2  16971  pythagtriplem1  17006  iserodd  17025  pcqmul  17043  pcexp  17049  pcneg  17064  pcmpt  17082  pcfac  17089  prmreclem2  17107  prmreclem3  17108  1arith  17117  vdwpc  17170  ramcl  17219  prmop1  17228  imasval  17695  ercpbllem  17732  iscat  17858  iscatd  17859  catideu  17861  iscatd2  17867  catlid  17869  catrid  17870  catass  17872  homfeq  17880  comfeq  17892  catpropd  17895  moni  17923  epii  17930  sectffval  17937  sectfval  17938  oppcsect  17965  sectmon  17969  isfunc  18051  funcid  18057  funcco  18058  funcpropd  18089  isfull  18099  fthsect  18114  fthmon  18116  natfval  18136  isnat  18137  nati  18145  fucsect  18162  natpropd  18166  setcmon  18274  setcepi  18275  setcsect  18276  fthestrcsetc  18336  embedsetcestrclem  18343  fthsetcestrc  18351  evlfcl  18408  uncfcurf  18425  yoniso  18471  joinval  18561  meetval  18575  islat  18619  latdisdlem  18682  latdisd  18683  isclat  18686  isdlat  18708  dlatmjdi  18709  isacs5lem  18731  acsdrscl  18732  acsficl  18733  isps  18754  mgmn0plusgplusf  18840  mgmidmo  18850  mgmlrid  18859  lidrideqd  18862  lidrididd  18863  grpinvalem  18866  grpinva  18867  mgmidpfod  18869  imasmgm2  18875  gsumvalx  18877  gsumval2  18887  ismgmhm  18897  mgmhmpropd  18899  mgmhmlin  18900  mgmhmeql  18917  issgrp  18921  isnsgrp  18924  sgrpass  18926  sgrp1  18930  issgrpd  18931  sgrppropd  18932  ismndd  18958  mndpropd  18963  imasmnd2  18980  xpsmnd0  18984  mnd1  18985  mnd1id  18986  ismhm  18992  mhmpropd  18999  mhmlin  19000  mhmimalem  19032  mhmeql  19034  gsumccat  19049  gsumwmhm  19053  frmdgsum  19070  symggrplem  19092  smndex1mndlem  19120  smndex1n0mnd  19123  sgrp2rid2  19137  sgrp2nmndlem4  19139  isgrp  19162  grppropd  19174  isgrpd2e  19178  dfgrp2  19185  isgrpid2  19199  grpidd2  19200  grpinvfval  19201  grpinvfvalALT  19202  grpinv11  19230  grpinvpropd  19237  grpidssd  19238  grpinvssd  19239  grpsubrcan  19243  dfgrp3lem  19260  grplactcnv  19265  imasgrp2  19277  mhmlem  19284  mulgnn0p1  19307  mulgaddcom  19320  mulginvcom  19321  mulgneg2  19330  mulgnnass  19331  mulgnn0ass  19332  mulgass  19333  mhmmulg  19337  cyccom  19430  isghm  19442  ghmlin  19447  ghmeql  19465  isga  19517  gagrpid  19520  gaass  19523  galcan  19530  orbsta  19539  cntzfval  19546  elcntz  19548  cntzsnval  19550  elcntzsn  19551  cntzi  19555  resscntz  19559  cntzmhm  19567  gsumwrev  19592  snsymgefmndeq  19621  cayleylem2  19639  symgextf1  19647  gsmsymgreqlem2  19657  gsmsymgreq  19658  symgfixf1  19663  pmtrfrn  19684  odfval  19758  odfvalALT  19759  mndodcong  19768  odbezout  19784  odeq1  19786  submod  19795  gexval  19804  gexdvds  19810  ispgp  19818  sylow1lem1  19824  sylow2alem1  19843  sylow2alem2  19844  sylow2blem2  19847  efgmnvl  19940  efgredlemc  19971  efgredeu  19978  frgpuptinv  19997  frgpup1  20001  frgpup3lem  20003  iscmn  20015  cmnpropd  20017  iscmnd  20020  abladdsub4  20037  submcmn2  20065  qusabl  20091  abl1  20092  imasabl  20102  iscyg  20105  cycsubmcmn  20115  gsum2dlem2  20197  telgsumfzs  20215  dmdprd  20226  dprdval  20231  dprdfcntz  20243  subgdmdprd  20262  dprd2da  20270  dpjrid  20290  pgpfac1lem3a  20304  ablfaclem3  20315  ablfac2  20317  gsumle  20371  isrng  20388  rngdi  20394  rngdir  20395  rngpropd  20408  imasrng  20411  ringurd  20423  issrg  20426  o2timesd  20448  rglcom4d  20449  srgmulgass  20455  srgpcomp  20456  srgbinom  20469  isring  20475  ringpropd  20531  ringinvnz1ne0  20543  mulgass2  20552  ring1  20553  imasring  20572  xpsring1d  20575  dvdsr  20604  dvreq1  20653  rnghmval  20682  isrnghm  20683  rnghmmul  20691  c0snmgmhm  20704  rngisomring1  20710  isrhm0  20718  crngrhmfo  20738  zrrnghm  20800  islring  20804  rngcsect  20900  ringcsect  20934  rrgval  20961  unitrrg  20967  domnlcanb  20983  domnrcanb  20985  isdrng  20996  drngprop  21010  isdrngd  21034  isdrngdOLD  21036  drngpropd  21039  cntzsdrg  21071  isabv  21080  abvmul  21090  issrng  21113  issrngd  21124  idsrngd  21125  islmod  21151  lmodlema  21152  islmodd  21153  lmodvsmmulgdi  21184  lmodprop2d  21211  rmodislmodlem  21216  rmodislmod  21217  islmhm  21314  lmhmlin  21322  islmhm2  21325  lmhmeql  21342  lmhmpropd  21360  islbs  21363  lbspropd  21386  rnglidlmsgrp  21546  rnglidlrng  21547  quscrng  21591  rngqiprngimfo  21609  islpir  21664  cnfldmulg  21722  cnfldexp  21723  prmirredlem  21790  pzriprnglem6  21804  pzriprnglem10  21808  pzriprnglem12  21810  chrcong  21845  zndvds  21867  znf1o  21869  znunit  21881  cygznlem3  21887  frgpcyg  21891  psgndiflemB  21918  isphl  21946  ipcj  21952  iporthcom  21953  ip2eq  21971  isphld  21972  phlpropd  21973  phlssphl  21977  ocvfval  21984  iscss  22001  ishil  22036  isobs  22038  obsip  22039  obslbs  22048  frlmphl  22099  isassa  22176  assalem  22177  isassad  22185  assapropd  22191  assamulgscm  22221  mvrf1  22305  mplmonmul  22357  mplcoe1  22358  mplcoe3  22359  mplcoe5lem  22360  mplcoe5  22361  evlslem1  22403  mpfrcl  22406  evlsval  22407  psdpw  22503  coe1tm  22604  ply1sclf1  22620  ply1coe  22628  eqcoe1ply1eq  22629  cply1coe0bi  22632  coe1fzgsumd  22634  ply1scleq  22635  ply1chr  22636  gsumply1eq  22639  evl1gsumd  22687  mat0dimcrng  22797  mat1ghm  22810  mat1mhm  22811  dmatcrng  22829  scmateALT  22839  scmatcrng  22848  scmatf1  22858  mvmumamul1  22881  mdetdiagid  22927  mdetralt  22935  mdetunilem1  22939  mdetunilem3  22941  mdetunilem4  22942  mdetunilem7  22945  mdetunilem9  22947  mdetuni0  22948  madugsum  22970  smadiadetr  23002  matunitlindflem1  23006  matunitlindflem2  23007  mat2pmatf1  23059  m2cpminvid2lem  23084  decpmataa0  23098  pmatcollpw2lem  23107  pm2mpf1  23129  chcoeffeqlem  23215  chcoeffeq  23216  cayhamlem3  23217  cayleyhamilton1  23222  isperf  23481  restperf  23514  cmpsub  23730  isconn  23743  2ndcsep  23790  elptr2  23905  ptbasin  23908  dfac14  23949  txcnp  23951  ptcnplem  23952  ptcnp  23953  cnmpt11  23994  cnmpt21  24002  cnmptcom  24009  kqfeq  24055  isr0  24068  pt1hmeo  24137  ustexsym  24547  isusp  24592  imasdsf1olem  24704  isxms  24778  xmspropd  24804  imasf1oxms  24820  stdbdmopn  24849  isngp3  24929  ngppropd  24968  tngngp3  24987  isnlm  25006  nmvs  25007  xrsxmet  25141  cnheibor  25288  htpyi  25307  htpycc  25313  pi1xfr  25388  pi1coghm  25394  isclm  25397  lmhmclm  25420  isclmp  25430  clmmulg  25434  iscph  25503  tcphcph  25570  cphsscph  25584  cmetcaulem  25621  bcth3  25664  ovolunlem1a  25829  ovolicc2lem1  25850  ovolicc2lem4  25853  ovolicc2  25855  mblsplit  25865  volun  25878  volfiniun  25880  voliunlem1  25883  volsup  25889  ioorinv  25909  uniioombllem2  25916  vitalilem3  25943  mbfeqalem1  25974  mbflim  26001  itgeqa  26146  itgconst  26151  itgfsum  26159  itgsplitioo  26170  dvnadd  26261  dvnres  26263  dvexp  26285  dvmptfsum  26307  mvth  26324  dvlip  26325  lhop1lem  26345  dvcvx  26352  mdegle0  26407  ply1nzb  26453  mon1pval  26472  facth1  26497  ig1pval  26506  dgrmulc  26602  dgrcolem1  26604  dgrcolem2  26605  dgrco  26606  coecj  26609  vieta1lem2  26646  vieta1  26647  elqaalem3  26656  dvntaylp  26710  ulmss  26736  mtest  26743  sineq0  26864  efif1olem4  26885  cxpexp  27008  mulcxplem  27024  mulcxp  27025  cxpmul2  27029  cxpeq  27097  affineequiv2  27164  quad2  27179  dcubic  27186  leibpi  27282  o1cxp  27314  scvxcvx  27325  facgam  27405  wilthlem1  27407  wilthlem2  27408  mpodvdsmulf1o  27533  fsumdvdsmul  27534  perfect  27570  dchrelbas2  27576  dchrinv  27600  dchrptlem2  27604  lgsne0  27674  lgsqrlem2  27686  lgsdchr  27694  gausslemma2d  27713  lgseisenlem2  27715  lgsquad2lem2  27724  2lgslem1a  27730  2lgslem1b  27731  dchrisumlem1  27828  qabvexp  27965  ostthlem1  27966  ostthlem2  27967  ostth3  27977  flt0  27981  ltsval2  28025  ltsres  28031  nolesgn2ores  28041  nogesgn1ores  28043  nolt02o  28064  nogt01o  28065  nosupcbv  28071  nosupno  28072  nosupdm  28073  nosupfv  28075  nosupres  28076  nosupbnd1lem1  28077  nosupbnd1lem3  28079  nosupbnd1lem5  28081  noinfcbv  28086  noinfno  28087  noinfdm  28088  noinffv  28090  noinfres  28091  noinfbnd1lem3  28094  noinfbnd1lem5  28096  addsrid  28362  addscom  28364  addscan1  28392  addsass  28403  subscan1d  28501  subscan2d  28502  mulsrid  28511  mulscom  28537  addsdilem3  28551  addsdilem4  28552  addsdi  28553  mulsasslem3  28563  mulsass  28564  mulscan2d  28577  mulscan1d  28578  bdayons  28674  om2noseqrdg  28702  n0cut  28732  expadds  28833  pw2cut  28858  pw2cut2  28860  elreno  28889  istrkgc  28928  istrkgcb  28930  istrkgld  28933  istrkg2ld  28934  axtgcgrrflx  28936  axtgupdim2  28945  tgjustf  28947  tgjustr  28948  iscgrg  28987  iscgrglt  28989  trgcgrg  28990  tgcgr4  29006  motcgr  29011  legso  29074  mirval  29139  israg  29184  ismidb  29295  isinagd  29370  angmgmaddov2  29401  angmgmval  29406  f1otrgds  29458  ttgval  29464  ttgitvval  29471  brcgr  29490  brbtwn2  29495  colinearalglem1  29496  colinearalg  29500  ax5seglem1  29518  ax5seglem2  29519  ax5seglem8  29526  ax5seglem9  29527  axlowdimlem13  29544  axlowdimlem16  29547  axlowdim1  29549  axcontlem1  29554  axcontlem2  29555  axcontlem6  29559  axcontlem7  29560  axcontlem8  29561  ecgrtg  29573  usgredg2v  29820  issubgr  29864  cplgruvtxb  30006  cusgrsize  30047  finsumvtxdg2size  30143  isrgr  30152  wkslem1  30200  wkslem2  30201  iswlk  30203  uspgr2wlkeq  30238  2wlklem  30258  wlkres  30261  redwlk  30263  wlkp1lem6  30269  wlkp1lem7  30270  wlkp1lem8  30271  pfxwlk  30278  revwlk  30279  pthdivtx  30324  upgrwlkdvdelem  30334  isclwlk  30372  iscrct  30389  iscycl  30390  crctcshwlkn0lem4  30414  crctcshwlkn0lem5  30415  crctcshwlkn0lem6  30416  wwlksnextinj  30500  rusgrnumwwlk  30579  clwlkclwwlklem2  30603  clwlkclwwlkf1lem3  30609  clwlkclwwlkf1  30613  erclwwlkeq  30621  clwwlkel  30649  clwwlkf  30650  clwwlkf1  30652  erclwwlkneq  30670  clwwlkvbij  30716  upgreupthseg  30822  eupth2eucrct  30830  eupth2lem3  30849  eupth2  30852  eucrctshift  30856  2clwwlk  30960  numclwwlk1lem2f1  30970  numclwlk1lem1  30982  numclwlk1lem2  30983  numclwlk2lem2f1o  30992  isgrpo  31111  grpoass  31117  grpoidinvlem3  31120  grpoidinv  31122  grpoideu  31123  grpoidinv2  31129  grpoinvfval  31136  isablo  31160  ablocom  31162  vciOLD  31175  vcidOLD  31178  vcdi  31179  vcdir  31180  vcass  31181  isvclem  31191  isnvlem  31224  nvmeq0  31272  nvs  31277  imsmetlem  31304  islno  31367  lnolin  31368  ishmo  31425  isphg  31431  phpar2  31437  phpar  31438  ipdiri  31444  ipasslem1  31445  ipasslem5  31449  ipasslem11  31454  ipassi  31455  dipdir  31456  dipass  31459  ip2eqi  31470  htth  31532  hvsubsub4  31674  hvnegdi  31681  hvaddcan  31684  hvaddcan2  31685  hvsubcan  31688  hvsubcan2  31689  hvaddsub4  31692  hial2eq  31720  normlem9at  31735  normsq  31748  norm-iii  31754  normsub  31757  normpyth  31759  normpar  31769  polid  31773  issubgoilem  31874  ococ  32020  chj0  32111  chlejb1  32126  chdmm1  32139  chjass  32147  spanun  32159  spansn  32173  elspansn2  32181  cmbr  32198  cmbr3  32222  pjoml2  32225  pjoml3  32226  osum  32259  spansnj  32261  pjch1  32284  pjadji  32299  pjaddi  32300  pjinormi  32301  pjsubi  32302  pjmuli  32303  pjcjt2  32306  pjch  32308  pjopyth  32334  pjpyth  32339  hoaddcom  32388  hoaddass  32396  hocsubdir  32399  hoaddrid  32405  ho0sub  32411  honegsub  32413  adjsym  32447  eigrei  32448  eigre  32449  eigposi  32450  eigorth  32452  ellnop  32472  elhmop  32487  ellnfn  32497  cnvadj  32506  lnopl  32528  unop  32529  hmop  32536  lnfnl  32545  adj1  32547  eleigvec  32571  hoddi  32604  lnopeq0lem2  32620  lnopunilem1  32624  lnopunilem2  32625  lnopunii  32626  elunop2  32627  lnophmi  32632  lnfnmul  32662  cnlnadjlem5  32685  branmfn  32719  bra11  32722  hmopidmchi  32765  hmopidmch  32767  hmopidmpj  32768  pjss2coi  32778  pjssmi  32779  pjssge0i  32780  pjidmco  32795  dfpjop  32796  elpjrn  32804  isst  32827  ishst  32828  hstel2  32833  stj  32849  mdbr  32908  mdi  32909  mdbr3  32911  dmdbr  32913  dmdmd  32914  dmdi  32916  dmdbr3  32919  mddmd2  32923  mdsl1i  32935  chjatom  32971  iuninc  33209  fmptcof2  33305  receqid  33389  bcm1n  33440  fsumiunle  33473  sgnsgn  33475  xmulcand  33540  xrsmulgzz  33623  psgnfzto1st  33719  isfxp  33782  fxpgaeq  33783  isslmd  33816  slmdlema  33817  gsumvsca1  33840  gsumvsca2  33841  urpropd  33844  elrgspnsubrunlem2  33862  erlval  33872  domnpropd  33894  qusvscpbl  33965  nsgqusf1olem3  34019  opprqusdrng  34070  ressply1mon1p  34153  ressply1invg  34154  deg1prod  34168  ply1moneq  34173  psrgsum  34233  psrmonmul  34235  psrmonprod  34237  vietalem  34264  vieta  34265  fedgmul  34316  brfldext  34330  fldextrspunlsplem  34358  extdgfialglem1  34377  bralgext  34382  minplyval  34390  submateq  34494  dispcmp  34544  pstmxmet  34582  cnre2csqlem  34595  mndpluscn  34611  qqhval2  34667  isrrext  34685  esumfzf  34754  esumcvg  34771  esum2dlem  34777  esumiun  34779  ofcfeqd2  34786  ismeas  34885  isrnmeas  34886  measvun  34895  carsgval  34988  inelcarsg  34996  carsgclctunlem1  35002  carsgclctunlem2  35004  pmeasmono  35009  pmeasadd  35010  eulerpartlemgvv  35061  eulerpartlemn  35066  sseqp1  35080  probun  35104  breprexp  35315  istrkg2d  35348  axtgupdim2ALTV  35350  afsval  35356  bnj1385  35515  bnj66  35543  bnj106  35551  bnj155  35562  bnj222  35566  bnj540  35575  bnj591  35594  bnj594  35595  bnj611  35601  bnj893  35611  bnj1000  35624  bnj966  35627  bnj1112  35666  bnj1234  35696  bnj1253  35700  bnj1280  35703  bnj1326  35709  bnj1450  35733  bnj1463  35738  bnj1529  35753  ecscottd  35823  brlexod  35953  brr0d  35955  subfacp1lem3  36068  subfacp1lem4  36069  subfacp1lem5  36070  subfacp1lem6  36071  subfacval2  36073  erdszelem9  36085  sconnpht  36115  ptpconn  36119  cvmliftmolem1  36167  cvmliftmolem2  36168  cvmliftlem10  36180  cvmlift2  36202  cvmliftphtlem  36203  satfdm  36255  gonarlem  36280  gonar  36281  goalr  36283  satfdmfmla  36286  prv  36314  mrsubff1  36400  mrsubccat  36404  elmrsubrn  36406  mrsubvrs  36408  elmpst  36422  msrid  36431  msubvrs  36446  cardprcr  36585  cardprcALT  36586  sqdivzi  36620  shftvalg  36624  bcprod  36630  bccolsum  36631  iprodefisumlem  36632  faclimlem1  36635  rdgprc  36683  dfrdg2  36684  elwlim  36712  fvsingle  36809  fullfunfv  36838  lineelsb2  37040  nmulprop  37066  nmulcom  37070  nmulrid  37073  nadddilem1  37096  nadddilem2  37097  nadddilem3  37098  nadddilem4  37099  nadddi  37100  opnregcld  37245  cldregopn  37246  neibastop3  37277  weiunval  37377  csbttc  37424  bj-sbeqALT  37939  bj-gabeqis  37978  bj-isclm  38352  rdgeqoa  38433  fvineqsnf1  38473  tan2h  38675  poimirlem9  38687  poimirlem13  38691  poimirlem14  38692  poimirlem16  38694  poimirlem19  38697  broucube  38712  voliunnfl  38722  volsupnfl  38723  findcard4  38772  cocanfo  38793  upixp  38803  sdclem2  38816  caushft  38835  ismtycnv  38876  ismtyima  38877  ismtybndlem  38880  ismtyres  38882  bfplem2  38897  bfp  38898  isass  38920  opidonOLD  38926  exidu1  38930  cmpidelt  38933  grpoeqdivid  38955  elghomlem2OLD  38960  ghomlinOLD  38962  ghomco  38965  isrngo  38971  rngoid  38976  rngoideu  38977  rngodi  38978  rngodir  38979  rngoass  38980  rngohomval  39038  isrngohom  39039  rngohomadd  39043  rngohommul  39044  iscom2  39069  iscringd  39072  crngocom  39075  crngohomfo  39080  dmncan2  39151  elsymrels4  39711  brredunds  39782  lshpset  40175  lcvexchlem4  40234  lcvexchlem5  40235  lflset  40256  islfl  40257  lfli  40258  islfld  40259  eqlkr3  40298  isopos  40377  oposlem  40379  opcon3b  40393  cmtvalN  40408  omllaw  40440  cvlexchb2  40528  cvlatexchb2  40532  cvlsupr2  40540  4atlem9  40800  4atlem10a  40801  4atlem11a  40804  4atlem12a  40807  4at2  40811  pmapglb2N  40968  pmapglb2xN  40969  paddasslem17  41033  ispsubclN  41134  ispsubcl2N  41144  lhpmod2i2  41235  lhpmod6i1  41236  4atexlemex2  41268  4atex  41273  4atex2-0aOLDN  41275  4atex2-0cOLDN  41277  ldilval  41310  ltrnfset  41314  ltrnset  41315  isltrn  41316  ltrneq2  41345  trnfsetN  41352  trnsetN  41353  istrnN  41354  cdlemd5  41399  cdleme0moN  41422  cdleme0nex  41487  cdleme18d  41492  cdleme31so  41576  cdleme31fv  41587  cdlemg2jlemOLDN  41790  cdlemg2fvlem  41791  cdlemg2klem  41792  istendo  41957  tendovalco  41962  tendoeq2  41971  dicelvalN  42375  dihval  42429  dihcnv11  42472  dihmeetlem13N  42516  dihlspsnat  42530  dochn0nv  42572  dochkrshp4  42586  lpolsetN  42679  lpolsatN  42685  lpolpolsatN  42686  lcfl1lem  42688  lclkrlem2a  42704  lclkrlem2e  42708  lcfls1lem  42731  lclkrs2  42737  lcdfval  42785  lcdval  42786  mapdffval  42823  mapdfval  42824  mapd0  42862  mapdpglem30  42899  mapdhval  42921  mapdheq2  42926  hdmap1vallem  42994  hdmap1val  42995  hdmap1cbv  42999  hdmapval3N  43035  hdmap10  43037  hdmapeq0  43041  hdmap14lem12  43076  hdmap14lem13  43077  hgmapfval  43083  hgmapvs  43088  hgmapvv  43123  hlhilocv  43154  recbothd  43182  lcmineqlem13  43231  isprimroot  43283  primrootsunit1  43287  aks6d1c1p1  43297  aks6d1c1p3  43300  aks6d1c1p4  43301  aks6d1c1p5  43302  evl1gprodd  43307  aks6d1c1rh  43315  aks6d1c2lem3  43316  deg1gprod  43330  deg1pow  43331  sticksstones22  43358  aks6d1c6lem2  43361  aks5lem3a  43379  unitscyglem2  43386  unitscyglem3  43387  unitscyglem4  43388  ccatcan2d  43442  remulcan2d  43447  sumcubes  43510  expeqidd  43522  cxp112d  43532  cxp111d  43533  log11d  43537  sn-addcand  43611  sn-addcan2d  43613  sn-mullid  43627  nn0addcom  43666  renegmulnnass  43669  nn0mulcom  43670  zmulcomlem  43671  cnreeu  43694  abvexp  43736  fiabv  43740  prjsprel  43772  prjcrvfval  43807  sn-isghm  43824  ismrcd2  43850  ismrc  43852  dvdsrabdioph  43957  fphpdo  43964  rmxypairf1o  44058  monotoddzzfi  44089  monotoddzz  44090  oddcomabszz  44091  rmxdioph  44163  expdiophlem2  44169  dnnumch3  44194  aomclem8  44203  islssfg  44212  unxpwdom3  44237  gicabl  44241  idomodle  44333  fgraphxp  44346  hausgraph  44347  onov0suclim  44416  oaabsb  44436  oaomoencom  44459  oenass  44461  omabs2  44474  tfsconcat0b  44488  nadd1suc  44534  naddonnn  44537  minregex  44675  relexpmulnn  44849  clsk1independent  45186  ntrclsk13  45211  ntrclsk4  45212  imo72b2  45312  grumnud  45410  nzss  45441  caofcan  45447  expgrowth  45459  fperiodmullem  46458  uzinico3  46713  fsumf1of  46725  fmuldfeq  46734  fprodexp  46745  fprodabs2  46746  climmulf  46755  climexp  46756  climsuse  46759  climrecf  46760  climaddf  46766  mullimc  46767  limcperiod  46779  neglimc  46796  addlimc  46797  0ellimcdiv  46798  climeldmeqmpt  46817  climfveqmpt  46820  climfveqf  46829  climfveqmpt3  46831  climeldmeqf  46832  climeqf  46837  climeldmeqmpt3  46838  limsupequz  46872  cncfperiod  47028  icccncfext  47036  fperdvper  47068  dvnmptdivc  47087  dvnxpaek  47091  dvnmul  47092  dvmptfprod  47094  dvnprodlem3  47097  itgspltprt  47128  stoweidlem30  47179  stoweidlem48  47197  wallispilem4  47217  wallispi2lem1  47220  wallispi2lem2  47221  fourierdlem50  47305  fourierdlem73  47328  fourierdlem81  47336  fourierdlem89  47344  fourierdlem90  47345  fourierdlem91  47346  fourierdlem92  47347  fourierdlem94  47349  fourierdlem97  47352  fourierdlem111  47366  fourierdlem112  47367  fourierdlem113  47368  sge0iunmptlemfi  47562  ismea  47600  meadjuni  47606  meaiuninclem  47629  caragenval  47642  isome  47643  caragensplit  47649  carageniuncllem1  47670  caratheodorylem1  47675  hoidmvlelem3  47746  vonvolmbllem  47809  vonvolmbl  47810  smflimlem3  47922  smflim  47926  smfpimcc  47957  smfsuplem2  47961  tmachlem-agreeself  48085  tmachlem-agreeprod  48086  fsetsnf1  48261  cfsetsnfsetf1  48268  fcoresf1  48278  csbafv12g  48346  csbaovg  48389  csbafv212g  48428  mod2addne  48579  fargshiftf1  48662  fargshiftfva  48664  prproropf1olem4  48727  fmtnorec2  48767  fmtnoprmfac1lem  48788  fmtnofac1  48794  quad1  48857  requad1  48859  perfectALTV  48960  fpprwppr  48976  nfermltl8rev  48979  nfermltl2rev  48980  nfermltlrev  48981  sbgoldbo  49024  isgrim  49119  grimuhgr  49124  grimcnv  49125  grimco  49126  uhgrimedgi  49127  isuspgrim0  49131  upgrimwlklem5  49138  gricushgr  49154  isubgrgrim  49166  uhgrimisgrgriclem  49167  clnbgrgrimlem  49170  clnbgrgrim  49171  grimedg  49172  uspgrlimlem3  49227  uspgrlimlem4  49228  grlimedgclnbgr  49232  grlimgrtrilem2  49239  gpgvtxedg0  49300  gpgvtxedg1  49301  uspgrsprf1  49384  plusfreseq  49400  iscomlaw  49426  isasslaw  49428  lidldomn1  49467  zlidlring  49470  rngcsectALTV  49511  ringcsectALTV  49545  idomcanr  49584  ovmpordxf  49590  lmodvsmdi  49630  islininds  49697  lindslinindimp2lem4  49712  lindslinindsimp2  49714  lmod1  49743  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  nn0sumshdiglem1  49872  nn0sumshdig  49874  1arymaptf1  49893  2arymaptf1  49904  itcovalpc  49923  itcovalt2  49928  rrx2pnecoorneor  49967  rrx2plordisom  49975  rrx2line  49991  rrx2linest  49993  line2ylem  50002  line2x  50005  line2y  50006  itscnhlc0yqe  50010  itscnhlc0xyqsol  50016  elovmpoeq  50119  idmon  50273  idepi  50274  sectpropdlem  50289  ssccatid  50325  imaidfu  50365  oppff1  50403  imasubc  50406  diag1f1lem  50567  diag2f1lem  50569  fucofvalne  50586  catcsect  50672  grptcmon  50870  grptcepi  50871  aacllem  51153