Theorem eqeq12d 2777

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  neeq12d  3017  cdeqeq  3733  sbceqg  4370  csbun  4399  csbin  4400  csbdif  4481  csbif  4540  iununi  5059  csbopab  5530  csbopabw  5531  dfid2  5548  csbima12  6076  dmsnsnsn  6221  csbcog  6300  dfpred3g  6316  preddowncl  6335  limeq  6374  csbiota  6531  fveqres  6929  opabiota  6967  fvmptf  7015  eqfnfv2f  7033  fsneq  7034  fvreseq0  7037  fveqdmss  7078  fvcofneq  7093  fnressn  7162  fnelfp  7180  fprb  7199  fnprb  7214  fntpb  7215  f1cofveqaeqALT  7262  f1resveqaeq  7277  nvocnv  7289  cocan1  7299  cocan2  7300  2fvcoidd  7305  fliftfun  7320  weniso  7364  csbriota  7392  oveqrspc2v  7447  csbov123  7464  eqfnov  7549  ovmpos  7568  ov2gf  7569  ovmpodxf  7570  caovcomg  7616  caovassg  7619  caovcang  7622  caovcanrd  7624  caovcan  7625  caovdig  7635  caovdirg  7638  caovmo  7658  coof  7717  offveqb  7720  caofid0l  7726  caofid0r  7727  caofidlcan  7731  caofass  7733  caonncan  7737  ordunisuc  7843  onsucuni2  7845  orduninsuc  7854  op1stg  8013  op2ndg  8014  f1o2ndf1  8133  xpord2pred  8162  xpord3pred  8169  poseq  8175  soseq  8176  fnsuppres  8208  csbfrecsg  8302  fpr3g  8303  frrlem1  8304  frrlem12  8315  frrlem13  8316  fpr2a  8320  wfr3g  8337  onfununi  8349  tfrlem1  8383  tfrlem3a  8384  tfrlem5  8387  tfrlem9  8393  tfrlem11  8396  tfrlem12  8397  tfr3  8407  tz7.44-1  8414  tz7.44-2  8415  tz7.44-3  8416  rdglem1  8423  rdg0g  8435  seqomlem1  8460  oalim  8540  omlim  8541  oelim  8542  oa0r  8546  om0r  8547  om1r  8551  oaass  8569  oarec  8570  odi  8587  omass  8588  oelim2  8604  oeoalem  8605  oeoa  8606  oeoelem  8607  oeoe  8608  nna0r  8618  nnacom  8626  nnaass  8631  nndi  8632  nnmass  8633  nnmsucr  8634  nnmcom  8635  oaabs  8657  oaabs2  8658  omabs  8660  naddcllem  8685  naddcom  8692  naddrid  8693  naddass  8706  naddsuc2  8711  naddoa  8712  ecovcom  8844  ecovass  8845  ecovdi  8846  dom2lem  9019  unxpdomlem2  9248  unxpdomlem3  9249  ixpfi2  9339  fipreima  9347  ordiso2  9509  wemaplem1  9540  wemaplem2  9541  wemapsolem  9544  cantnfval2  9670  cantnfp1lem3  9681  oemapvali  9685  cantnflem1c  9688  cantnflem1  9690  wemapwe  9698  rnttrcl  9723  tcvalg  9737  frr3g  9760  frr2  9764  rankvalg  9826  rankonidlem  9838  rankpwg  9857  ranklim  9858  rankung  9873  ranksng  9874  rankuni  9879  updjud  10015  cardprclem  10060  cardprc  10061  carduni  10062  fseqenlem1  10103  fodomacn  10135  alephcard  10149  alephfp2  10188  alephval3  10189  dfac12lem1  10222  dfac12lem2  10223  dfac12r  10225  ackbij1lem8  10304  ackbij1lem14  10310  ackbij1lem16  10312  ackbij2lem3  10318  cardcf  10329  sornom  10355  fin23lem28  10418  isf32lem2  10432  itunitc  10499  ituniiun  10500  axdc3lem2  10529  axdc4lem  10533  ttukeylem3  10589  ttukey2g  10594  fpwwe2lem7  10722  fpwwecbv  10729  canth4  10732  pwfseqlem2  10744  addcanpi  10984  mulcanpi  10985  recrecnq  11052  ltexnq  11060  genpv  11084  0idsr  11182  1idsr  11183  ax1rid  11246  mulrid  11306  addcan  11494  addcan2  11495  mulcand  11949  mulcan2d  11950  mulcan2g  11970  divmuleq  12022  conjmul  12034  eqneg  12037  ofsubeq0  12317  nnadd1com  12361  nnaddcom  12362  nnadddir  12394  nnmul1com  12395  nnmulcom  12396  rpnnen1lem6  13110  cnref1o  13113  xmulasslem  13415  xmulass  13417  xadddi2  13427  prunioo  13612  fzsuc2  13716  fzprval  13719  fztpval  13720  fzosplitprm1  13913  modadd1  14048  modaddb  14049  modmul1  14067  addmodlteq  14089  om2uzsuci  14091  om2uzrdg  14099  uzrdgxfr  14110  seq1  14157  seqp1  14159  seqfveq2  14167  seqfveq  14169  seqshft2  14171  seqsplit  14178  seqcaopr3  14180  seqcaopr2  14181  seqf1olem2a  14183  seqf1olem2  14185  seqf1o  14186  seqid  14190  seqid2  14191  seqhomo  14192  ser1const  14201  seqof2  14203  mulexp  14244  expadd  14247  expmul  14250  binom2  14361  sq01  14369  modexp  14382  bcpasc  14465  hashgadd  14521  hashdom  14523  hashfzo  14574  hashfzp1  14576  hashxplem  14578  hashxp  14579  hashmap  14580  hashpw  14581  hashbclem  14597  hashbc  14598  hashfacen  14599  hashf1lem1  14600  hashf1lem2  14601  hashf1  14602  seqcoll  14609  eqs1  14760  swrdspsleq  14815  pfxeq  14845  pfxsuff1eqwrdeq  14848  ccatopth2  14866  cats1un  14870  swrdccatin1  14874  swrdccat3blem  14888  cshf1  14961  repswcshw  14963  s2eq2s1eq  15087  s3eqs2s1eq  15089  pfx2  15098  2swrd2eqwrdeq  15106  wwlktovf1  15110  eqwrds3  15114  relexpsucnnr  15178  relexpsucnnl  15183  relexpcnv  15188  relexpaddnn  15204  replim  15283  cjreb  15290  cjexp  15317  absexp  15471  abs1m  15503  recan  15504  cnsqrt00  15560  isercoll2  15836  iseraltlem2  15850  iseraltlem3  15851  sumeq2ii  15860  zsum  15884  fsum  15886  fsumf1o  15889  sumss  15890  fsumcvg2  15893  fsumadd  15906  isummulc2  15928  fsum2d  15937  fsummulc2  15950  fsumconst  15956  modfsummods  15960  modfsummod  15961  fsumparts  15973  fsumrelem  15974  fsumiun  15988  binom  15999  bcxmas  16004  incexclem  16005  isumshft  16008  isumnn0nn  16011  climcndslem1  16018  climcndslem2  16019  mertenslem2  16054  clim2prod  16057  prodfrec  16064  prodeq2ii  16080  zprod  16104  fprod  16108  fprodf1o  16113  fprodser  16116  fprodmul  16127  fproddiv  16128  prodsn  16129  prodsnf  16131  fprodabs  16141  fprodconst  16145  fprod2d  16148  fprodmodd  16164  binomfallfac  16207  bpolydif  16221  fprodefsum  16261  efne0d  16263  efne0OLD  16265  efexp  16269  demoivreALT  16369  moddvds  16433  bitsinv1  16612  sadadd2  16630  smu01lem  16655  smupval  16658  smueqlem  16660  smumullem  16662  gcdaddm  16697  bezoutlem1  16712  bezout  16716  gcddiv  16724  seq1st  16746  alginv  16750  algfx  16755  lcmneg  16778  lcmid  16784  lcmgcdeq  16787  lcmfunsnlem1  16812  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem  16816  lcmfunsn  16819  lcmfun  16820  divgcdcoprm0  16840  cncongr1  16842  cncongr2  16843  nn0gcdsq  16928  crth  16955  eulerthlem2  16959  pythagtriplem1  16994  iserodd  17013  pcqmul  17031  pcexp  17037  pcneg  17052  pcmpt  17070  pcfac  17077  prmreclem2  17095  prmreclem3  17096  1arith  17105  vdwpc  17158  ramcl  17207  prmop1  17216  imasval  17683  ercpbllem  17720  iscat  17846  iscatd  17847  catideu  17849  iscatd2  17855  catlid  17857  catrid  17858  catass  17860  homfeq  17868  comfeq  17880  catpropd  17883  moni  17911  epii  17918  sectffval  17925  sectfval  17926  oppcsect  17953  sectmon  17957  isfunc  18039  funcid  18045  funcco  18046  funcpropd  18077  isfull  18087  fthsect  18102  fthmon  18104  natfval  18124  isnat  18125  nati  18133  fucsect  18150  natpropd  18154  setcmon  18262  setcepi  18263  setcsect  18264  fthestrcsetc  18324  embedsetcestrclem  18331  fthsetcestrc  18339  evlfcl  18396  uncfcurf  18413  yoniso  18459  joinval  18549  meetval  18563  islat  18607  latdisdlem  18670  latdisd  18671  isclat  18674  isdlat  18696  dlatmjdi  18697  isacs5lem  18719  acsdrscl  18720  acsficl  18721  isps  18742  mgmn0plusgplusf  18828  mgmidmo  18838  mgmlrid  18847  lidrideqd  18850  lidrididd  18851  grpinvalem  18854  grpinva  18855  mgmidpfod  18857  imasmgm2  18863  gsumvalx  18865  gsumval2  18875  ismgmhm  18885  mgmhmpropd  18887  mgmhmlin  18888  mgmhmeql  18905  issgrp  18909  isnsgrp  18912  sgrpass  18914  sgrp1  18918  issgrpd  18919  sgrppropd  18920  ismndd  18946  mndpropd  18951  imasmnd2  18968  xpsmnd0  18972  mnd1  18973  mnd1id  18974  ismhm  18980  mhmpropd  18987  mhmlin  18988  mhmimalem  19020  mhmeql  19022  gsumccat  19037  gsumwmhm  19041  frmdgsum  19058  symggrplem  19080  smndex1mndlem  19108  smndex1n0mnd  19111  sgrp2rid2  19125  sgrp2nmndlem4  19127  isgrp  19150  grppropd  19162  isgrpd2e  19166  dfgrp2  19173  isgrpid2  19187  grpidd2  19188  grpinvfval  19189  grpinvfvalALT  19190  grpinv11  19218  grpinvpropd  19225  grpidssd  19226  grpinvssd  19227  grpsubrcan  19231  dfgrp3lem  19248  grplactcnv  19253  imasgrp2  19265  mhmlem  19272  mulgnn0p1  19295  mulgaddcom  19308  mulginvcom  19309  mulgneg2  19318  mulgnnass  19319  mulgnn0ass  19320  mulgass  19321  mhmmulg  19325  cyccom  19418  isghm  19430  ghmlin  19435  ghmeql  19453  isga  19505  gagrpid  19508  gaass  19511  galcan  19518  orbsta  19527  cntzfval  19534  elcntz  19536  cntzsnval  19538  elcntzsn  19539  cntzi  19543  resscntz  19547  cntzmhm  19555  gsumwrev  19580  snsymgefmndeq  19609  cayleylem2  19627  symgextf1  19635  gsmsymgreqlem2  19645  gsmsymgreq  19646  symgfixf1  19651  pmtrfrn  19672  odfval  19746  odfvalALT  19747  mndodcong  19756  odbezout  19772  odeq1  19774  submod  19783  gexval  19792  gexdvds  19798  ispgp  19806  sylow1lem1  19812  sylow2alem1  19831  sylow2alem2  19832  sylow2blem2  19835  efgmnvl  19928  efgredlemc  19959  efgredeu  19966  frgpuptinv  19985  frgpup1  19989  frgpup3lem  19991  iscmn  20003  cmnpropd  20005  iscmnd  20008  abladdsub4  20025  submcmn2  20053  qusabl  20079  abl1  20080  imasabl  20090  iscyg  20093  cycsubmcmn  20103  gsum2dlem2  20185  telgsumfzs  20203  dmdprd  20214  dprdval  20219  dprdfcntz  20231  subgdmdprd  20250  dprd2da  20258  dpjrid  20278  pgpfac1lem3a  20292  ablfaclem3  20303  ablfac2  20305  gsumle  20359  isrng  20376  rngdi  20382  rngdir  20383  rngpropd  20396  imasrng  20399  ringurd  20411  issrg  20414  o2timesd  20436  rglcom4d  20437  srgmulgass  20443  srgpcomp  20444  srgbinom  20457  isring  20463  ringpropd  20519  ringinvnz1ne0  20531  mulgass2  20540  ring1  20541  imasring  20560  xpsring1d  20563  dvdsr  20592  dvreq1  20641  rnghmval  20670  isrnghm  20671  rnghmmul  20679  c0snmgmhm  20692  rngisomring1  20698  isrhm0  20706  crngrhmfo  20726  zrrnghm  20788  islring  20792  rngcsect  20888  ringcsect  20922  rrgval  20949  unitrrg  20955  domnlcanb  20971  domnrcanb  20973  isdrng  20984  drngprop  20998  isdrngd  21022  isdrngdOLD  21024  drngpropd  21027  cntzsdrg  21059  isabv  21068  abvmul  21078  issrng  21101  issrngd  21112  idsrngd  21113  islmod  21139  lmodlema  21140  islmodd  21141  lmodvsmmulgdi  21172  lmodprop2d  21199  rmodislmodlem  21204  rmodislmod  21205  islmhm  21302  lmhmlin  21310  islmhm2  21313  lmhmeql  21330  lmhmpropd  21348  islbs  21351  lbspropd  21374  rnglidlmsgrp  21534  rnglidlrng  21535  quscrng  21579  rngqiprngimfo  21597  islpir  21652  cnfldmulg  21710  cnfldexp  21711  prmirredlem  21778  pzriprnglem6  21792  pzriprnglem10  21796  pzriprnglem12  21798  chrcong  21833  zndvds  21855  znf1o  21857  znunit  21869  cygznlem3  21875  frgpcyg  21879  psgndiflemB  21906  isphl  21934  ipcj  21940  iporthcom  21941  ip2eq  21959  isphld  21960  phlpropd  21961  phlssphl  21965  ocvfval  21972  iscss  21989  ishil  22024  isobs  22026  obsip  22027  obslbs  22036  frlmphl  22087  isassa  22164  assalem  22165  isassad  22173  assapropd  22179  assamulgscm  22209  mvrf1  22293  mplmonmul  22345  mplcoe1  22346  mplcoe3  22347  mplcoe5lem  22348  mplcoe5  22349  evlslem1  22391  mpfrcl  22394  evlsval  22395  psdpw  22491  coe1tm  22592  ply1sclf1  22608  ply1coe  22616  eqcoe1ply1eq  22617  cply1coe0bi  22620  coe1fzgsumd  22622  ply1scleq  22623  ply1chr  22624  gsumply1eq  22627  evl1gsumd  22675  mat0dimcrng  22785  mat1ghm  22798  mat1mhm  22799  dmatcrng  22817  scmateALT  22827  scmatcrng  22836  scmatf1  22846  mvmumamul1  22869  mdetdiagid  22915  mdetralt  22923  mdetunilem1  22927  mdetunilem3  22929  mdetunilem4  22930  mdetunilem7  22933  mdetunilem9  22935  mdetuni0  22936  madugsum  22958  smadiadetr  22990  matunitlindflem1  22994  matunitlindflem2  22995  mat2pmatf1  23047  m2cpminvid2lem  23072  decpmataa0  23086  pmatcollpw2lem  23095  pm2mpf1  23117  chcoeffeqlem  23203  chcoeffeq  23204  cayhamlem3  23205  cayleyhamilton1  23210  isperf  23469  restperf  23502  cmpsub  23718  isconn  23731  2ndcsep  23778  elptr2  23893  ptbasin  23896  dfac14  23937  txcnp  23939  ptcnplem  23940  ptcnp  23941  cnmpt11  23982  cnmpt21  23990  cnmptcom  23997  kqfeq  24043  isr0  24056  pt1hmeo  24125  ustexsym  24535  isusp  24580  imasdsf1olem  24692  isxms  24766  xmspropd  24792  imasf1oxms  24808  stdbdmopn  24837  isngp3  24917  ngppropd  24956  tngngp3  24975  isnlm  24994  nmvs  24995  xrsxmet  25129  cnheibor  25276  htpyi  25295  htpycc  25301  pi1xfr  25376  pi1coghm  25382  isclm  25385  lmhmclm  25408  isclmp  25418  clmmulg  25422  iscph  25491  tcphcph  25558  cphsscph  25572  cmetcaulem  25609  bcth3  25652  ovolunlem1a  25817  ovolicc2lem1  25838  ovolicc2lem4  25841  ovolicc2  25843  mblsplit  25853  volun  25866  volfiniun  25868  voliunlem1  25871  volsup  25877  ioorinv  25897  uniioombllem2  25904  vitalilem3  25931  mbfeqalem1  25962  mbflim  25989  itgeqa  26134  itgconst  26139  itgfsum  26147  itgsplitioo  26158  dvnadd  26249  dvnres  26251  dvexp  26273  dvmptfsum  26295  mvth  26312  dvlip  26313  lhop1lem  26333  dvcvx  26340  mdegle0  26395  ply1nzb  26441  mon1pval  26460  facth1  26485  ig1pval  26494  dgrmulc  26590  dgrcolem1  26592  dgrcolem2  26593  dgrco  26594  coecj  26597  vieta1lem2  26634  vieta1  26635  elqaalem3  26644  dvntaylp  26698  ulmss  26724  mtest  26731  sineq0  26852  efif1olem4  26873  cxpexp  26996  mulcxplem  27012  mulcxp  27013  cxpmul2  27017  cxpeq  27085  affineequiv2  27152  quad2  27167  dcubic  27174  leibpi  27270  o1cxp  27302  scvxcvx  27313  facgam  27393  wilthlem1  27395  wilthlem2  27396  mpodvdsmulf1o  27521  fsumdvdsmul  27522  perfect  27558  dchrelbas2  27564  dchrinv  27588  dchrptlem2  27592  lgsne0  27662  lgsqrlem2  27674  lgsdchr  27682  gausslemma2d  27701  lgseisenlem2  27703  lgsquad2lem2  27712  2lgslem1a  27718  2lgslem1b  27719  dchrisumlem1  27816  qabvexp  27953  ostthlem1  27954  ostthlem2  27955  ostth3  27965  flt0  27969  ltsval2  28013  ltsres  28019  nolesgn2ores  28029  nogesgn1ores  28031  nolt02o  28052  nogt01o  28053  nosupcbv  28059  nosupno  28060  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  noinfcbv  28074  noinfno  28075  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem3  28082  noinfbnd1lem5  28084  addsrid  28350  addscom  28352  addscan1  28380  addsass  28391  subscan1d  28489  subscan2d  28490  mulsrid  28499  mulscom  28525  addsdilem3  28539  addsdilem4  28540  addsdi  28541  mulsasslem3  28551  mulsass  28552  mulscan2d  28565  mulscan1d  28566  bdayons  28662  om2noseqrdg  28690  n0cut  28720  expadds  28821  pw2cut  28846  pw2cut2  28848  elreno  28877  istrkgc  28916  istrkgcb  28918  istrkgld  28921  istrkg2ld  28922  axtgcgrrflx  28924  axtgupdim2  28933  tgjustf  28935  tgjustr  28936  iscgrg  28975  iscgrglt  28977  trgcgrg  28978  tgcgr4  28994  motcgr  28999  legso  29062  mirval  29127  israg  29172  ismidb  29283  isinagd  29358  angmgmaddov2  29389  angmgmval  29394  f1otrgds  29446  ttgval  29452  ttgitvval  29459  brcgr  29478  brbtwn2  29483  colinearalglem1  29484  colinearalg  29488  ax5seglem1  29506  ax5seglem2  29507  ax5seglem8  29514  ax5seglem9  29515  axlowdimlem13  29532  axlowdimlem16  29535  axlowdim1  29537  axcontlem1  29542  axcontlem2  29543  axcontlem6  29547  axcontlem7  29548  axcontlem8  29549  ecgrtg  29561  usgredg2v  29808  issubgr  29852  cplgruvtxb  29994  cusgrsize  30035  finsumvtxdg2size  30131  isrgr  30140  wkslem1  30188  wkslem2  30189  iswlk  30191  uspgr2wlkeq  30226  2wlklem  30246  wlkres  30249  redwlk  30251  wlkp1lem6  30257  wlkp1lem7  30258  wlkp1lem8  30259  pfxwlk  30266  revwlk  30267  pthdivtx  30312  upgrwlkdvdelem  30322  isclwlk  30360  iscrct  30377  iscycl  30378  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem6  30404  wwlksnextinj  30488  rusgrnumwwlk  30567  clwlkclwwlklem2  30591  clwlkclwwlkf1lem3  30597  clwlkclwwlkf1  30601  erclwwlkeq  30609  clwwlkel  30637  clwwlkf  30638  clwwlkf1  30640  erclwwlkneq  30658  clwwlkvbij  30704  upgreupthseg  30810  eupth2eucrct  30818  eupth2lem3  30837  eupth2  30840  eucrctshift  30844  2clwwlk  30948  numclwwlk1lem2f1  30958  numclwlk1lem1  30970  numclwlk1lem2  30971  numclwlk2lem2f1o  30980  isgrpo  31099  grpoass  31105  grpoidinvlem3  31108  grpoidinv  31110  grpoideu  31111  grpoidinv2  31117  grpoinvfval  31124  isablo  31148  ablocom  31150  vciOLD  31163  vcidOLD  31166  vcdi  31167  vcdir  31168  vcass  31169  isvclem  31179  isnvlem  31212  nvmeq0  31260  nvs  31265  imsmetlem  31292  islno  31355  lnolin  31356  ishmo  31413  isphg  31419  phpar2  31425  phpar  31426  ipdiri  31432  ipasslem1  31433  ipasslem5  31437  ipasslem11  31442  ipassi  31443  dipdir  31444  dipass  31447  ip2eqi  31458  htth  31520  hvsubsub4  31662  hvnegdi  31669  hvaddcan  31672  hvaddcan2  31673  hvsubcan  31676  hvsubcan2  31677  hvaddsub4  31680  hial2eq  31708  normlem9at  31723  normsq  31736  norm-iii  31742  normsub  31745  normpyth  31747  normpar  31757  polid  31761  issubgoilem  31862  ococ  32008  chj0  32099  chlejb1  32114  chdmm1  32127  chjass  32135  spanun  32147  spansn  32161  elspansn2  32169  cmbr  32186  cmbr3  32210  pjoml2  32213  pjoml3  32214  osum  32247  spansnj  32249  pjch1  32272  pjadji  32287  pjaddi  32288  pjinormi  32289  pjsubi  32290  pjmuli  32291  pjcjt2  32294  pjch  32296  pjopyth  32322  pjpyth  32327  hoaddcom  32376  hoaddass  32384  hocsubdir  32387  hoaddrid  32393  ho0sub  32399  honegsub  32401  adjsym  32435  eigrei  32436  eigre  32437  eigposi  32438  eigorth  32440  ellnop  32460  elhmop  32475  ellnfn  32485  cnvadj  32494  lnopl  32516  unop  32517  hmop  32524  lnfnl  32533  adj1  32535  eleigvec  32559  hoddi  32592  lnopeq0lem2  32608  lnopunilem1  32612  lnopunilem2  32613  lnopunii  32614  elunop2  32615  lnophmi  32620  lnfnmul  32650  cnlnadjlem5  32673  branmfn  32707  bra11  32710  hmopidmchi  32753  hmopidmch  32755  hmopidmpj  32756  pjss2coi  32766  pjssmi  32767  pjssge0i  32768  pjidmco  32783  dfpjop  32784  elpjrn  32792  isst  32815  ishst  32816  hstel2  32821  stj  32837  mdbr  32896  mdi  32897  mdbr3  32899  dmdbr  32901  dmdmd  32902  dmdi  32904  dmdbr3  32907  mddmd2  32911  mdsl1i  32923  chjatom  32959  iuninc  33155  fmptcof2  33251  receqid  33336  bcm1n  33387  fsumiunle  33420  sgnsgn  33422  xmulcand  33487  xrsmulgzz  33570  psgnfzto1st  33666  isfxp  33729  fxpgaeq  33730  isslmd  33763  slmdlema  33764  gsumvsca1  33787  gsumvsca2  33788  urpropd  33791  elrgspnsubrunlem2  33809  erlval  33819  domnpropd  33841  qusvscpbl  33912  nsgqusf1olem3  33966  opprqusdrng  34017  ressply1mon1p  34100  ressply1invg  34101  deg1prod  34115  ply1moneq  34120  psrgsum  34180  psrmonmul  34182  psrmonprod  34184  vietalem  34211  vieta  34212  fedgmul  34263  brfldext  34277  fldextrspunlsplem  34305  extdgfialglem1  34324  bralgext  34329  minplyval  34337  submateq  34441  dispcmp  34491  pstmxmet  34529  cnre2csqlem  34542  mndpluscn  34558  qqhval2  34614  isrrext  34632  esumfzf  34701  esumcvg  34718  esum2dlem  34724  esumiun  34726  ofcfeqd2  34733  ismeas  34832  isrnmeas  34833  measvun  34842  carsgval  34935  inelcarsg  34943  carsgclctunlem1  34949  carsgclctunlem2  34951  pmeasmono  34956  pmeasadd  34957  eulerpartlemgvv  35008  eulerpartlemn  35013  sseqp1  35027  probun  35051  breprexp  35262  istrkg2d  35295  axtgupdim2ALTV  35297  afsval  35303  bnj1385  35462  bnj66  35490  bnj106  35498  bnj155  35509  bnj222  35513  bnj540  35522  bnj591  35541  bnj594  35542  bnj611  35548  bnj893  35558  bnj1000  35571  bnj966  35574  bnj1112  35613  bnj1234  35643  bnj1253  35647  bnj1280  35650  bnj1326  35656  bnj1450  35680  bnj1463  35685  bnj1529  35700  subfacp1lem3  35947  subfacp1lem4  35948  subfacp1lem5  35949  subfacp1lem6  35950  subfacval2  35952  erdszelem9  35964  sconnpht  35994  ptpconn  35998  cvmliftmolem1  36046  cvmliftmolem2  36047  cvmliftlem10  36059  cvmlift2  36081  cvmliftphtlem  36082  satfdm  36134  gonarlem  36159  gonar  36160  goalr  36162  satfdmfmla  36165  prv  36193  mrsubff1  36279  mrsubccat  36283  elmrsubrn  36285  mrsubvrs  36287  elmpst  36301  msrid  36310  msubvrs  36325  sqdivzi  36493  shftvalg  36497  bcprod  36503  bccolsum  36504  iprodefisumlem  36505  faclimlem1  36508  rdgprc  36556  dfrdg2  36557  elwlim  36585  fvsingle  36682  fullfunfv  36711  lineelsb2  36913  nmulprop  36939  nmulcom  36943  nmulrid  36946  nadddilem1  36969  nadddilem2  36970  nadddilem3  36971  nadddilem4  36972  nadddi  36973  opnregcld  37118  cldregopn  37119  neibastop3  37150  weiunval  37250  csbttc  37297  bj-sbeqALT  37812  bj-gabeqis  37851  bj-isclm  38212  rdgeqoa  38293  fvineqsnf1  38333  tan2h  38535  poimirlem9  38547  poimirlem13  38551  poimirlem14  38552  poimirlem16  38554  poimirlem19  38557  broucube  38572  voliunnfl  38582  volsupnfl  38583  findcard4  38632  cocanfo  38653  upixp  38663  sdclem2  38676  caushft  38695  ismtycnv  38736  ismtyima  38737  ismtybndlem  38740  ismtyres  38742  bfplem2  38757  bfp  38758  isass  38780  opidonOLD  38786  exidu1  38790  cmpidelt  38793  grpoeqdivid  38815  elghomlem2OLD  38820  ghomlinOLD  38822  ghomco  38825  isrngo  38831  rngoid  38836  rngoideu  38837  rngodi  38838  rngodir  38839  rngoass  38840  rngohomval  38898  isrngohom  38899  rngohomadd  38903  rngohommul  38904  iscom2  38929  iscringd  38932  crngocom  38935  crngohomfo  38940  dmncan2  39011  elsymrels4  39571  brredunds  39642  lshpset  40035  lcvexchlem4  40094  lcvexchlem5  40095  lflset  40116  islfl  40117  lfli  40118  islfld  40119  eqlkr3  40158  isopos  40237  oposlem  40239  opcon3b  40253  cmtvalN  40268  omllaw  40300  cvlexchb2  40388  cvlatexchb2  40392  cvlsupr2  40400  4atlem9  40660  4atlem10a  40661  4atlem11a  40664  4atlem12a  40667  4at2  40671  pmapglb2N  40828  pmapglb2xN  40829  paddasslem17  40893  ispsubclN  40994  ispsubcl2N  41004  lhpmod2i2  41095  lhpmod6i1  41096  4atexlemex2  41128  4atex  41133  4atex2-0aOLDN  41135  4atex2-0cOLDN  41137  ldilval  41170  ltrnfset  41174  ltrnset  41175  isltrn  41176  ltrneq2  41205  trnfsetN  41212  trnsetN  41213  istrnN  41214  cdlemd5  41259  cdleme0moN  41282  cdleme0nex  41347  cdleme18d  41352  cdleme31so  41436  cdleme31fv  41447  cdlemg2jlemOLDN  41650  cdlemg2fvlem  41651  cdlemg2klem  41652  istendo  41817  tendovalco  41822  tendoeq2  41831  dicelvalN  42235  dihval  42289  dihcnv11  42332  dihmeetlem13N  42376  dihlspsnat  42390  dochn0nv  42432  dochkrshp4  42446  lpolsetN  42539  lpolsatN  42545  lpolpolsatN  42546  lcfl1lem  42548  lclkrlem2a  42564  lclkrlem2e  42568  lcfls1lem  42591  lclkrs2  42597  lcdfval  42645  lcdval  42646  mapdffval  42683  mapdfval  42684  mapd0  42722  mapdpglem30  42759  mapdhval  42781  mapdheq2  42786  hdmap1vallem  42854  hdmap1val  42855  hdmap1cbv  42859  hdmapval3N  42895  hdmap10  42897  hdmapeq0  42901  hdmap14lem12  42936  hdmap14lem13  42937  hgmapfval  42943  hgmapvs  42948  hgmapvv  42983  hlhilocv  43014  recbothd  43042  lcmineqlem13  43091  isprimroot  43143  primrootsunit1  43147  aks6d1c1p1  43157  aks6d1c1p3  43160  aks6d1c1p4  43161  aks6d1c1p5  43162  evl1gprodd  43167  aks6d1c1rh  43175  aks6d1c2lem3  43176  deg1gprod  43190  deg1pow  43191  sticksstones22  43218  aks6d1c6lem2  43221  aks5lem3a  43239  unitscyglem2  43246  unitscyglem3  43247  unitscyglem4  43248  ccatcan2d  43302  remulcan2d  43307  sumcubes  43370  expeqidd  43382  cxp112d  43392  cxp111d  43393  log11d  43397  sn-addcand  43471  sn-addcan2d  43473  sn-mullid  43487  nn0addcom  43526  renegmulnnass  43529  nn0mulcom  43530  zmulcomlem  43531  cnreeu  43554  abvexp  43596  fiabv  43600  prjsprel  43632  prjcrvfval  43667  sn-isghm  43684  ismrcd2  43709  ismrc  43711  dvdsrabdioph  43816  fphpdo  43823  rmxypairf1o  43917  monotoddzzfi  43948  monotoddzz  43949  oddcomabszz  43950  rmxdioph  44022  expdiophlem2  44028  dnnumch3  44053  aomclem8  44062  islssfg  44071  unxpwdom3  44096  gicabl  44100  idomodle  44192  fgraphxp  44205  hausgraph  44206  onov0suclim  44275  oaabsb  44295  oaomoencom  44318  oenass  44320  omabs2  44333  tfsconcat0b  44347  nadd1suc  44393  naddonnn  44396  minregex  44534  relexpmulnn  44708  clsk1independent  45045  ntrclsk13  45070  ntrclsk4  45071  imo72b2  45171  grumnud  45269  nzss  45300  caofcan  45306  expgrowth  45318  fperiodmullem  46318  uzinico3  46573  fsumf1of  46585  fmuldfeq  46594  fprodexp  46605  fprodabs2  46606  climmulf  46615  climexp  46616  climsuse  46619  climrecf  46620  climaddf  46626  mullimc  46627  limcperiod  46639  neglimc  46656  addlimc  46657  0ellimcdiv  46658  climeldmeqmpt  46677  climfveqmpt  46680  climfveqf  46689  climfveqmpt3  46691  climeldmeqf  46692  climeqf  46697  climeldmeqmpt3  46698  limsupequz  46732  cncfperiod  46888  icccncfext  46896  fperdvper  46928  dvnmptdivc  46947  dvnxpaek  46951  dvnmul  46952  dvmptfprod  46954  dvnprodlem3  46957  itgspltprt  46988  stoweidlem30  47039  stoweidlem48  47057  wallispilem4  47077  wallispi2lem1  47080  wallispi2lem2  47081  fourierdlem50  47165  fourierdlem73  47188  fourierdlem81  47196  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem92  47207  fourierdlem94  47209  fourierdlem97  47212  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  sge0iunmptlemfi  47422  ismea  47460  meadjuni  47466  meaiuninclem  47489  caragenval  47502  isome  47503  caragensplit  47509  carageniuncllem1  47530  caratheodorylem1  47535  hoidmvlelem3  47606  vonvolmbllem  47669  vonvolmbl  47670  smflimlem3  47782  smflim  47786  smfpimcc  47817  smfsuplem2  47821  tmachlem-agreeself  47945  tmachlem-agreeprod  47946  fsetsnf1  48121  cfsetsnfsetf1  48128  fcoresf1  48138  csbafv12g  48206  csbaovg  48249  csbafv212g  48288  mod2addne  48439  fargshiftf1  48522  fargshiftfva  48524  prproropf1olem4  48587  fmtnorec2  48627  fmtnoprmfac1lem  48648  fmtnofac1  48654  quad1  48717  requad1  48719  perfectALTV  48820  fpprwppr  48836  nfermltl8rev  48839  nfermltl2rev  48840  nfermltlrev  48841  sbgoldbo  48884  isgrim  48979  grimuhgr  48984  grimcnv  48985  grimco  48986  uhgrimedgi  48987  isuspgrim0  48991  upgrimwlklem5  48998  gricushgr  49014  isubgrgrim  49026  uhgrimisgrgriclem  49027  clnbgrgrimlem  49030  clnbgrgrim  49031  grimedg  49032  uspgrlimlem3  49087  uspgrlimlem4  49088  grlimedgclnbgr  49092  grlimgrtrilem2  49099  gpgvtxedg0  49160  gpgvtxedg1  49161  uspgrsprf1  49244  plusfreseq  49260  iscomlaw  49286  isasslaw  49288  lidldomn1  49327  zlidlring  49330  rngcsectALTV  49371  ringcsectALTV  49405  idomcanr  49444  ovmpordxf  49450  lmodvsmdi  49490  islininds  49557  lindslinindimp2lem4  49572  lindslinindsimp2  49574  lmod1  49603  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem1  49732  nn0sumshdig  49734  1arymaptf1  49753  2arymaptf1  49764  itcovalpc  49783  itcovalt2  49788  rrx2pnecoorneor  49826  rrx2plordisom  49834  rrx2line  49851  rrx2linest  49853  line2ylem  49862  line2x  49865  line2y  49866  itscnhlc0yqe  49870  itscnhlc0xyqsol  49876  idmon  50127  idepi  50128  sectpropdlem  50143  ssccatid  50179  imaidfu  50217  oppff1  50255  imasubc  50258  diag1f1lem  50413  diag2f1lem  50415  fucofvalne  50432  catcsect  50505  grptcmon  50700  grptcepi  50701  aacllem  50938