Theorem 3eqtr3d 2780

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2774	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2774	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  reldisjun  6032  mpteqb  7017  fvmptt  7018  fvsnun2  7183  fsnunfv  7187  f1ocnvfv1  7276  f1ocnvfv2  7277  fcof1  7287  f1ofvswap  7306  weniso  7353  caov12d  7630  caov13d  7632  caov411d  7634  caovmo  7646  onovuni  8344  tfrlem5  8382  seqomlem1  8452  seqomlem4  8455  onasuc  8530  onesuc  8532  oeeui  8604  nadd4  8699  fopwdom  9082  unxpdomlem2  9253  cantnfres  9674  cnfcom2lem  9698  cnfcom2  9699  updjud  9931  cardiun  9979  ackbij1lem16  10232  ackbij2lem2  10237  fpwwe2lem5  10632  fpwwe2lem7  10634  canthp1lem2  10650  mul12  11383  mul4  11386  addrid  11398  addcan  11402  addcom  11404  addcomd  11420  add12  11435  ppncan  11506  addsub4  11507  subeqxfrd  11627  subaddeqd  11633  muladd  11650  mulcand  11851  receu  11863  div13  11897  divdivdiv  11919  divcan5  11920  divdiv1  11929  divdiv2  11930  halfaddsub  12449  xadddi  13278  xov1plusxeqvd  13479  fztp  13561  flzadd  13795  fldiv  13829  mulp1mod1  13881  modnegd  13895  modsub12d  13897  2submod  13901  seqm1  13989  seqcaopr  14009  seqf1o  14013  exprec  14073  expsub  14080  zesq  14193  digit1  14204  discr1  14206  discr  14207  facnn2  14246  faclbnd6  14263  hashfz1  14310  hashdom  14343  hashun  14346  hashbclem  14415  hashfac  14423  seqcoll  14429  ccatopth  14670  repsw2  14905  repsw3  14906  shftval3  15027  crre  15065  resub  15078  imsub  15086  cjsub  15100  nn0sqeq1  15227  abslem2  15290  sqreulem  15310  bhmafibid1  15416  climshft2  15530  isercolllem2  15616  iseraltlem2  15633  iseraltlem3  15634  fsumsub  15738  telfsumo  15752  telfsumo2  15753  hashiun  15772  bcxmas  15785  climcndslem1  15799  climcndslem2  15800  trireciplem  15812  geoser  15817  geo2sum2  15824  fprodm1  15915  fallfacfwd  15984  binomfallfaclem2  15988  bpolydiflem  16002  bpoly4  16007  fsumcube  16008  sinsub  16115  cossub  16116  rpnnen2lem10  16170  ruclem12  16188  p1modz1  16208  mod2eq1n2dvds  16294  pwp1fsum  16338  divalglem9  16348  bitsinv1lem  16386  bitsinv1  16387  bitsf1  16391  sadasslem  16415  bitsres  16418  smup1  16434  smumul  16438  modgcd  16478  absmulgcd  16495  eucalg  16528  lcmgcd  16548  lcmid  16550  lcmftp  16577  numdensq  16694  dfphi2  16711  phiprm  16714  fermltl  16721  prmdiveq  16723  hashgcdlem  16725  odzdvds  16732  powm2modprm  16740  modprm0  16742  coprimeprodsq  16745  pythagtriplem6  16758  pythagtriplem7  16759  pythagtriplem12  16763  pythagtriplem16  16767  pcaddlem  16825  sumhash  16833  pcfac  16836  pockthlem  16842  prmreclem6  16858  4sqlem12  16893  4sqlem15  16896  vdwlem3  16920  vdwlem6  16923  vdwlem9  16926  ramub1lem2  16964  cshwshashlem2  17034  qusaddvallem  17501  xpsaddlem  17523  xpsvsca  17527  mrcun  17570  homfeqval  17645  comfeqval  17656  sectcan  17706  sectco  17707  sectmon  17733  monsect  17734  funcsect  17826  setcmon  18041  resscatc  18063  catciso  18065  evlfcllem  18178  curf2cl  18188  curfcl  18189  yonedalem4c  18234  yonedalem3b  18236  yonedainv  18238  latj12  18441  grprinvlem  18598  grpinva  18599  grprida  18600  mnd12g  18672  resmhm  18737  pwsco2mhm  18750  frmdup3lem  18783  grprcan  18894  grplcan  18921  grpasscan1  18922  grpinv11  18928  grpinvnz  18930  grplmulf1o  18933  grpinvpropd  18934  grpinvadd  18937  grpsubsub4  18952  dfgrp3  18958  imasgrp2  18974  mhmid  18982  mhmmnd  18983  mulgz  19018  mulgdirlem  19021  mulgdir  19022  mulgass  19027  mulgsubdir  19030  mulgpropd  19032  pwsmulg  19035  isnsg3  19076  nmzsubg  19081  ssnmz  19082  eqger  19094  eqglact  19095  qus0subgadd  19114  cyccom  19118  ghminv  19137  conjnmz  19166  subgga  19205  gasubg  19207  galcan  19209  gacan  19210  cntzsubg  19244  cntzmhm  19246  symgvalstruct  19305  symgvalstructOLD  19306  psgnunilem2  19404  psgnuni  19408  sylow1lem1  19507  sylow2blem2  19530  sylow2blem3  19531  lsmmod  19584  lsmpropd  19586  lsmdisj2  19591  subgdisj1  19600  subgdisj2  19601  efgredleme  19652  efgredlemd  19653  efgredlemc  19654  efgredlem  19656  frgpup3lem  19686  mulgdi  19735  ghmcmn  19740  lsm4  19769  gsummhm2  19848  gsumpt  19871  gsum2d  19881  gsumcom3  19887  dprdfeq0  19933  ablfac1eu  19984  ablsimpgprmd  20026  rnglz  20059  rngrz  20060  isrngd  20067  rglcom4d  20105  ringcom  20168  isringd  20179  ring1eq0  20186  ringmneg1  20192  gsumdixp  20207  pwsexpg  20217  unitgrp  20274  irredrmul  20318  rngisom1  20357  rhmunitinv  20402  subrginv  20478  subrgunit  20480  drngmul0or  20529  isdrngd  20533  primefld  20564  abvrec  20587  srngnvl  20607  srngadd  20608  srngmul  20609  issrngd  20612  lmodvs0  20650  lmodvneg1  20659  lmodcom  20662  lmodsubdi  20673  lmodvsinv  20791  lmodvsinv2  20792  lmhmvsca  20800  lvecvs0or  20866  lvecinv  20871  lspsnvs  20872  lspabs2  20878  lspfixed  20886  lspsolv  20901  rngqiprnglinlem1  21050  rng2idl1cntr  21064  unitrrg  21109  prmirredlem  21243  mulgrhm2  21249  chrrhm  21302  znidomb  21336  psgnghm  21352  psgninv  21354  zrhpsgnodpm  21364  evpmodpmf1o  21368  psgndiflemB  21372  ip0r  21409  ipdir  21411  ipdi  21412  ipass  21417  ipassr  21418  phlpropd  21427  ocvpj  21491  uvcresum  21567  lmimlbs  21610  asclpropd  21670  psrass1lemOLD  21712  psrass1lem  21715  psrlidm  21742  psrridm  21743  mvrf1  21764  mplmon2mul  21849  evlslem1  21864  evlseu  21865  evlssca  21871  evlsvar  21872  coe1pwmul  22021  pf1ind  22094  mat0dimbas0  22188  mdetrlin  22324  mdetrsca  22325  mdetr0  22327  mdetunilem8  22341  mdetuni0  22343  mdetmul  22345  maducoeval2  22362  madurid  22366  madulid  22367  matinv  22399  matunit  22400  slesolinv  22402  slesolinvbi  22403  cpmadugsumlemF  22598  restin  22890  cncmp  23116  cmpsublem  23123  conndisj  23140  cnconn  23146  kgencmp2  23270  ufldom  23686  tgplacthmeo  23827  ghmcnp  23839  qustgpopn  23844  qustgphaus  23847  tsmsxplem2  23878  tususp  23997  xpsdsval  24107  blpnfctr  24162  xmssym  24191  ressxms  24254  isngp2  24326  ngppropd  24366  nminvr  24406  blcvx  24534  icccvx  24690  pcohtpylem  24759  pcohtpy  24760  clmvscom  24830  cvsmuleqdivd  24874  cvsdiveqd  24875  pjthlem1  25178  ovollb2lem  25229  ovolicc2lem1  25258  ovolicc2lem5  25262  volsup  25297  ovolioo  25309  uniiccdif  25319  uniioombllem3  25326  uniioombllem4  25327  vitalilem3  25351  itg1sub  25451  itg2const  25482  iblcnlem1  25529  itgcnlem  25531  itgaddlem2  25565  itgsub  25567  itgabs  25576  ditgsplit  25602  dvmulbr  25680  dvcmul  25685  dvcmulf  25686  dvrec  25696  dvmptres3  25697  dvmptadd  25701  dvmptmul  25702  dvmptres2  25703  dvmptneg  25707  dvmptsub  25708  dvmptcj  25709  dvmptco  25713  dveflem  25720  dvlip  25734  dvlipcn  25735  dvlip2  25736  dvcvx  25761  dvfsumle  25762  dvfsumabs  25764  dvfsumlem1  25767  dvfsumlem2  25768  ftc2  25785  ftc2ditglem  25786  itgparts  25788  itgsubstlem  25789  itgsubst  25790  itgpowd  25791  fta1glem1  25907  fta1blem  25910  plyeq0lem  25948  plymullem1  25952  coeeulem  25962  coe0  25994  coesub  25995  dvply1  26021  plydivlem4  26033  plyrem  26042  fta1lem  26044  vieta1  26049  plyexmo  26050  elqaalem2  26057  aareccl  26063  aannenlem1  26065  aaliou3lem2  26080  dvtaylp  26106  taylthlem1  26109  radcnvlem1  26149  pserdvlem2  26164  efcvx  26185  ptolemy  26230  tangtx  26239  efif1olem3  26277  efif1olem4  26278  efabl  26283  lognegb  26322  efiarg  26339  cosargd  26340  tanarg  26351  logtayl  26392  cxpneg  26413  cxpsub  26414  cxprec  26418  cxproot  26422  cxpsqrt  26435  cxpcom  26471  cxpcn3lem  26479  cxpaddlelem  26483  abscxpbnd  26485  root1eq1  26487  cxpeq  26489  logrec  26492  isosctrlem2  26548  isosctrlem3  26549  isosctr  26550  ssscongptld  26551  chordthmlem  26561  heron  26567  quad2  26568  dcubic1lem  26572  mcubic  26576  cubic2  26577  cubic  26578  dquartlem2  26581  dquart  26582  quart1lem  26584  quart1  26585  asinlem2  26598  asinlem3  26600  asinsin  26621  sinacos  26634  atanlogsublem  26644  efiatan2  26646  2efiatan  26647  tanatan  26648  atantan  26652  atans2  26660  dvatan  26664  atantayl  26666  atantayl2  26667  log2cnv  26673  rlimcnp2  26695  cxplim  26700  cxp2lim  26705  cvxcl  26713  scvxcvx  26714  zetacvg  26743  lgamgulmlem4  26760  lgamcvg2  26783  gamp1  26786  wilthlem1  26796  wilthlem2  26797  ftalem5  26805  basellem3  26811  basellem5  26813  basellem8  26816  mumullem2  26908  musum  26919  musumsum  26920  muinv  26921  sgmppw  26924  1sgmprm  26926  1sgm2ppw  26927  ppiub  26931  logfac2  26944  chpchtsum  26946  perfectlem1  26956  perfectlem2  26957  dchrn0  26977  dchrfi  26982  dchrabs  26987  dchrptlem1  26991  dchrhash  26998  dchr2sum  27000  sum2dchr  27001  bposlem6  27016  bposlem9  27019  lgsvalmod  27043  lgsdilem  27051  lgsne0  27062  lgssq  27064  lgssq2  27065  lgsqr  27078  lgsdchrval  27081  lgsdchr  27082  gausslemma2dlem6  27099  gausslemma2d  27101  lgseisenlem1  27102  lgseisenlem2  27103  lgseisenlem4  27105  lgsquadlem1  27107  lgsquadlem3  27109  lgsquad3  27114  m1lgs  27115  2sqmod  27163  rplogsumlem1  27211  rplogsumlem2  27212  dchrisumlem2  27217  dchrisum0fno1  27238  rpvmasum2  27239  dchrisum0lem1  27243  dchrisum0lem2  27245  mudivsum  27257  mulog2sumlem1  27261  vmalogdivsum  27266  2vmadivsumlem  27267  logsqvma  27269  selberglem1  27272  selberglem2  27273  selberg2lem  27277  selberg3lem1  27284  selberg4lem1  27287  selberg4  27288  pntrsumo1  27292  selbergr  27295  selberg34r  27298  pntrlog2bndlem3  27306  pntrlog2bndlem4  27307  pntibndlem2  27318  pntlemg  27325  pntlemr  27329  pntlemf  27332  ostthlem1  27354  padicabvcxp  27359  ostth3  27365  nolesgn2o  27398  nolesgn2ores  27399  nogesgn1o  27400  nogesgn1ores  27401  nodenselem5  27415  nolt02o  27422  nogt01o  27423  nosupprefixmo  27427  noinfprefixmo  27428  sltlpss  27626  slelss  27627  adds12d  27718  adds4d  27719  addsdilem3  27835  mulnegs1d  27842  muls12d  27860  norecdiv  27865  tgcgrcomlr  27986  tgifscgr  28014  iscgrglt  28020  tgbtwnconn1lem2  28079  tgbtwnconn1lem3  28080  mirne  28173  miduniq2  28193  krippenlem  28196  ragcgr  28213  cgrg3col4  28359  f1otrg  28377  ttgcontlem1  28397  brbtwn2  28418  axsegconlem10  28439  ax5seglem3  28444  ax5seglem6  28447  axpaschlem  28453  axeuclidlem  28475  axcontlem2  28478  axcontlem7  28483  axcontlem8  28484  cusgrsizeindslem  28963  frgrncvvdeq  29817  numclwwlk7  29899  nrt2irr  29981  grpoidinvlem1  30012  grpoideu  30017  grporcan  30026  grpolcan  30038  grpoinvop  30041  ablo4  30058  nvscom  30137  nvmul0or  30158  nvz0  30176  smcnlem  30205  ipidsq  30218  sspz  30243  lno0  30264  lnoadd  30266  lnomul  30268  ipasslem3  30341  dipdi  30351  dipassr  30354  dipsubdi  30357  ubthlem2  30379  hvmul0or  30533  hvadd12  30543  hvadd4  30544  hvmulcom  30551  normneg  30652  pjhthlem1  30899  chj12  31042  spanunsni  31087  5oalem2  31163  3oalem2  31171  hoadd4  31292  homul12  31313  hosubdi  31316  honegsubdi  31318  hosub4  31321  adj2  31442  lnopmul  31475  lnopaddi  31479  lnfnaddi  31551  lnfnmuli  31552  cnlnadjlem6  31580  adjeq0  31599  leopmul  31642  opsqrlem1  31648  opsqrlem6  31653  hstnmoc  31731  strlem1  31758  chirredlem3  31900  2ndresdju  32129  suppovss  32161  cosnop  32172  fpwrelmapffslem  32212  xaddeq0  32221  bcm1n  32261  divnumden2  32279  xmulcand  32342  xreceu  32343  s3f1  32368  ccatf1  32370  wrdt2ind  32372  swrdf1  32375  xrsmulgzz  32434  xrge0adddir  32448  xrge0adddi  32449  abliso  32452  gsumhashmul  32466  ogrpaddltrbid  32496  ogrpinvlt  32499  symgcom  32502  cyc2fv1  32538  cyc2fv2  32539  cycpmco2rn  32542  cycpmco2lem5  32547  cycpmco2lem6  32548  cycpmco2lem7  32549  cyc3fv1  32554  cyc3fv2  32555  cyc3fv3  32556  cycpmconjvlem  32558  cycpmconjslem2  32572  cycpmconjs  32573  cyc3conja  32574  archiabllem1a  32595  archiabllem1  32597  archiabllem2c  32599  slmdvs0  32628  dvrcan5  32643  ringinveu  32652  ornglmullt  32683  orngrmullt  32684  qusvsval  32725  imaslmod  32726  qustriv  32738  fermltlchr  32740  znfermltl  32741  quslsm  32778  qus0g  32780  nsgmgclem  32784  ghmquskerlem1  32790  rhmquskerlem  32805  qsidomlem2  32834  mxidlprm  32848  mxidlirredi  32849  opprqusbas  32864  qsdrngilem  32870  evls1fpws  32908  evls1addd  32910  evls1muld  32911  evls1vsca  32912  ressply10g  32918  ply1fermltlchr  32924  ply1fermltl  32925  r1padd1  32941  r1plmhm  32943  sradrng  32946  resssra  32950  drgext0gsca  32954  rlmdim  32970  rgmoddimOLD  32971  matdim  32976  ply1degltdimlem  32983  ply1degltdim  32984  lbsdiflsp0  32987  dimkerim  32988  fedgmullem1  32990  fedgmullem2  32991  fedgmul  32992  extdg1id  33018  ccfldextdgrr  33023  minplyirred  33047  algextdeglem8  33057  algextdeg  33058  mdetpmtr2  33090  madjusmdetlem1  33093  mdetlap  33098  qtophaus  33102  zarcmplem  33147  qqhval2lem  33247  esumpad  33339  esummulc1  33365  esumsup  33373  measxun2  33494  measssd  33499  inelcarsg  33596  carsggect  33603  carsgclctunlem2  33604  pmeasmono  33609  oddpwdc  33639  eulerpartlemgs2  33665  eulerpartlemn  33666  totprobd  33711  signstfvn  33866  signstfveq0  33874  ftc2re  33896  itgexpif  33904  breprexpnat  33932  circlemethnat  33939  circlevma  33940  circlemethhgt  33941  hgt750lemf  33951  hgt750lemg  33952  hgt750lemb  33954  tgoldbachgt  33961  bnj1379  34127  bnj1321  34324  revpfxsfxrev  34392  revwlk  34401  subfaclim  34465  cvxsconn  34520  resconn  34523  cvmliftmolem1  34558  cvmliftlem7  34568  cvmliftlem13  34573  cvmlift2lem7  34586  cvmlift3lem5  34600  elmsta  34825  msubff1  34833  mthmpps  34859  bcm1nt  34999  faclim2  35010  funsseq  35031  gg-dvmulbr  35461  gg-dvfsumle  35468  gg-dvfsumlem2  35469  clsun  35516  topjoin  35553  bj-bary1lem  36494  irrdifflemf  36509  finxpreclem4  36578  matunitlindflem1  36787  ptrest  36790  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem9  36800  poimirlem11  36802  poimirlem12  36803  poimirlem26  36817  poimirlem27  36818  itg2addnclem  36842  itg2addnclem3  36844  itgaddnclem2  36850  itgsubnc  36853  iblmulc2nc  36856  itgabsnc  36860  ftc2nc  36873  areacirclem1  36879  areacirclem4  36882  areacirc  36884  cocanfo  36890  ablo4pnp  37051  rngolz  37093  rngorz  37094  zerdivemp1x  37118  crngm4  37174  crngohomfo  37177  lfl0  38238  lfladd  38239  lflmul  38241  eqlkr3  38274  olm11  38400  latm12  38403  cmtcomlemN  38421  omlspjN  38434  hlatj12  38544  1cvrjat  38649  dalemrotyz  38832  padd12N  39013  pmapjlln1  39029  atmod2i1  39035  pmapocjN  39104  pnonsingN  39107  pexmidN  39143  lhp2at0  39206  lhpelim  39211  ltrncnv  39320  cdleme7c  39419  cdleme15b  39449  cdlemednpq  39473  cdleme20m  39497  cdleme22cN  39516  cdleme22d  39517  cdleme23b  39524  cdleme30a  39552  cdleme35h  39630  cdlemeg46frv  39699  cdlemg2fv2  39774  cdlemg2l  39777  cdlemg2m  39778  cdlemg8c  39803  cdlemg10bALTN  39810  cdlemg12  39824  cdlemg13a  39825  cdlemg18c  39854  cdlemg19  39858  trlcoat  39897  cdlemg47  39910  tendo1ne0  40002  cdlemk9  40013  cdlemk9bN  40014  dia2dimlem1  40238  tendolinv  40279  tendorinv  40280  dvhlveclem  40282  doca3N  40301  dihmeetlem7N  40484  dihjatc1  40485  dihmeetlem18N  40498  dochnoncon  40565  dihjatc  40591  dihjatcclem1  40592  dihjatcclem4  40595  dochsnkr  40646  lcfl7lem  40673  lcfl8  40676  lcfl9a  40679  lclkrlem1  40680  lclkrlem2e  40685  lclkrlem2j  40690  lcfrlem1  40716  lcfrlem9  40724  lcfrlem23  40739  lcfrlem31  40747  mapd0  40839  mapdpglem21  40866  baerlem3lem1  40881  baerlem5alem1  40882  mapdindp4  40897  mapdh6gN  40916  hdmap1l6g  40990  hgmapval0  41066  hgmaprnlem1N  41070  hlhilhillem  41138  crng12d  41392  imacrhmcl  41393  drngmulcanad  41403  drngmulcan2ad  41404  drnginvmuld  41405  evlsbagval  41440  sn-1ne2  41481  oddnumth  41511  sumcubes  41513  exp11d  41518  numdenexp  41530  resubeulem2  41551  resubidaddlidlem  41569  sn-00idlem1  41573  readdcan2  41587  sn-negex12  41591  sn-addcand  41594  remulinvcom  41607  remullid  41608  remulcand  41613  sn-0tie0  41614  zaddcomlem  41626  zaddcom  41627  zmulcomlem  41630  zmulcom  41631  retire  41642  cnreeu  41643  prjspner1  41670  dffltz  41678  flt4lem5f  41701  flt4lem7  41703  fltnltalem  41706  fltnlta  41707  diophrw  41799  eldioph2lem1  41800  pellexlem2  41870  pellexlem6  41874  pellex  41875  pell1234qrne0  41893  pell1234qrreccl  41894  pell1qrgaplem  41913  rmxm1  41975  oddcomabszz  41985  jm2.19lem1  42030  jm3.1lem2  42059  dnnumch3  42091  pwssplit4  42133  flcidc  42218  deg1mhm  42251  dflim5  42381  omabs2  42384  sqrtcval  42694  radcnvrat  43375  nzprmdif  43380  hashnzfz  43381  dvsconst  43391  dvsid  43392  expgrowth  43396  bccm1k  43403  bccn1  43405  binomcxplemnotnn0  43417  subadd4b  44291  uzinico2  44574  sumnnodd  44645  limsupresuz  44718  limsupequzlem  44737  liminfresre  44794  liminfresuz  44799  climliminflimsupd  44816  icccncfext  44902  dvresntr  44933  itgsinexplem1  44969  itgsinexp  44970  stoweidlem1  45016  wallispi2lem2  45087  stirlinglem3  45091  stirlinglem5  45093  stirlinglem10  45098  stirlinglem15  45103  dirkertrigeqlem3  45115  dirkercncflem2  45119  fourierdlem26  45148  fourierdlem42  45164  fourierdlem66  45187  fourierdlem73  45194  fourierdlem81  45202  fourierdlem83  45204  fourierdlem107  45228  etransclem23  45272  meaiininclem  45501  vonvolmbl  45676  iccvonmbllem  45693  sigaradd  45881  cevathlem1  45882  imarnf1pr  46289  m1mod0mod1  46336  fmtnorec3  46515  proththd  46581  perfectALTVlem1  46688  perfectALTVlem2  46689  pw2m1lepw2m1  47289  nnpw2pmod  47357  dignn0flhalflem1  47389  affinecomb2  47477  1subrec1sub  47479  eenglngeehlnmlem1  47511  2itscplem3  47554  restcls2  47634  aacllem  47936  amgmlemALT  47938  young2d  47940