Theorem 3eqtrrd 2802

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

Hypotheses

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

Assertion

Ref	Expression
3eqtrrd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2797	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2798	1 ⊢ (𝜑 → 𝐷 = 𝐴)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  fimacnvinrn  7066  fvcofneq  7088  iunfictbso  10105  axcnre  11155  fseq1p1m1  13633  seqf1olem1  14084  expmulz  14151  expubnd  14221  subsq  14253  bcm1k  14358  bcpasc  14364  cshwcshid  14871  crim  15173  rereb  15178  rlimrecl  15638  iseraltlem2  15741  fsumsplit1  15803  fsumparts  15865  isumshft  15900  geoserg  15927  pwdif  15929  efsub  16162  sincossq  16238  efieq1re  16261  nn0expgcd  16628  eucalg  16651  lcmfunsnlem  16705  phiprmpw  16841  modprmn0modprm0  16873  coprimeprodsq  16874  pythagtriplem15  16895  pythagtriplem17  16897  fldivp1  16963  1arithlem4  16992  setsidvald  17265  setsid  17273  pwsbas  17546  invfuc  18040  estrreslem1  18199  latdisdlem  18558  ghmquskerco  19360  odinv  19637  frgpuplem  19848  gexexlem  19928  fincygsubgodd  20190  srgbinomlem4  20317  gsumdixp  20407  c0snmgmhm  20551  funcrngcsetc  20750  funcringcsetc  20784  cnfldsub  21561  mplcoe1  22199  evlsvarsrng  22269  selvvvval  22304  psdmul  22340  ply1coe  22469  evls1varsrng  22511  mat1scmat  22707  m1detdiag  22765  mdetunilem7  22786  madugsum  22811  pm2mpmhmlem2  22987  mretopd  23260  upxp  23791  uptx  23793  imasdsf1olem  24541  clmvs2  25264  cphipipcj  25370  cphipval2  25411  itgmulc2lem2  26003  r1pid  26329  coeeulem  26392  fta1lem  26479  aaliou3lem8  26519  eff1olem  26724  tanarg  26795  logcnlem4  26821  root1cj  26932  angpieqvdlem  27004  quad2  27015  dcubic  27022  quart1  27032  jensen  27164  lgamgulmlem5  27208  lgamgulm2  27211  ftalem5  27252  basellem8  27263  chpchtsum  27394  logfaclbnd  27397  perfectlem2  27405  gausslemma2dlem1a  27540  2sqlem3  27595  dchrvmasum2lem  27671  dchrvmasumiflem2  27677  selberglem2  27721  selberg3r  27744  pntlem3  27784  ostth2  27812  ostth3  27813  madeoldsuc  28089  zseo  28626  addhalfcut  28663  pw2cut2  28666  krippenlem  28978  colinearalglem1  29267  axlowdimlem16  29318  axcontlem4  29328  clwlkclwwlkfo  30371  nmbdoplbi  32387  nmcopexi  32390  nmbdfnlbi  32412  nmcfnexi  32414  nmcfnlbi  32415  hstoh  32595  fcobij  33076  lt2addrd  33106  xlt2addrd  33115  cshwrnid  33290  symgfcoeu  33411  cycpmconjslem2  33484  cycpmconjs  33485  isarchi3  33516  archirngz  33518  elrgspnsubrunlem1  33576  elrspunsn  33746  mxidlirredi  33763  1arithidomlem1  33834  1arithidomlem2  33835  1arithidom  33836  evlextv  33941  esplyfval1  33972  dimkerim  34026  lvecendof1f1o  34032  fldextrspunlsplem  34072  nn0constr  34160  constraddcl  34161  constrnegcl  34162  constrremulcl  34166  constrrecl  34168  constrimcl  34169  constrmulcl  34170  constrreinvcl  34171  constrinvcl  34172  constrresqrtcl  34176  constrabscl  34177  2sqr3minply  34179  submatminr1  34209  mdetpmtr1  34222  madjusmdetlem1  34226  zarcmplem  34280  qqhnm  34389  esumfzf  34468  ddemeas  34635  sseqp1  34794  ballotlemi1  34902  ballotlemii  34903  ballotlemic  34906  ballotlem1c  34907  fsum2dsub  35003  circlemeth  35036  hgt750lemb  35052  hgt750lema  35053  hgt750leme  35054  elmrsubrn  36020  nadddilem1  36720  cos2h  38290  itg2addnclem  38350  itgmulc2nclem2  38366  areacirclem1  38387  areacirclem4  38390  cntotbnd  38475  atmod2i2  40664  trljat1  40968  trljat2  40969  cdleme9  41055  cdleme15b  41077  cdleme20c  41113  cdleme22eALTN  41147  dvhopN  41918  doca2N  41928  cdlemn10  42008  dochocss  42168  djhlj  42203  dihprrnlem1N  42226  dihprrnlem2  42227  lcfl7lem  42301  lclkrlem2c  42311  hgmapadd  42696  hdmapinvlem3  42722  hgmapvvlem1  42725  sumcubes  43102  zaddcomlem  43265  fidomncyc  43331  rmydbl  43695  jm2.18  43743  jm2.19  43748  proot1hash  43950  dssmapnvod  44774  binomcxplemnotnn0  45094  oddfl  46025  dstregt0  46029  supsubc  46097  absimlere  46221  uzinico2  46305  mccllem  46341  ellimcabssub0  46361  sumnnodd  46374  climresmpt  46401  limsupresuz  46445  liminfresuz  46526  coskpi2  46608  cosknegpi  46611  dvsinax  46655  dvnmptdivc  46680  dvnxpaek  46684  dvnmul  46685  dvmptfprodlem  46686  ditgeqiooicc  46702  itgioocnicc  46719  itgspltprt  46721  wallispi2lem2  46814  dirkerper  46838  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem18  46867  fourierdlem19  46868  fourierdlem33  46882  fourierdlem35  46884  fourierdlem41  46890  fourierdlem42  46891  fourierdlem48  46896  fourierdlem49  46897  fourierdlem50  46898  fourierdlem53  46901  fourierdlem63  46911  fourierdlem65  46913  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem81  46929  fourierdlem82  46930  fourierdlem83  46931  fourierdlem84  46932  fourierdlem90  46938  fourierdlem93  46941  fourierdlem95  46943  fourierdlem103  46951  fourierdlem104  46952  fourierdlem107  46955  fourierdlem111  46959  fourierswlem  46972  fouriersw  46973  etransclem4  46980  etransclem9  46985  etransclem28  47004  etransclem35  47011  etransclem38  47014  sge0tsms  47122  sge0sup  47133  sge0resplit  47148  sge0split  47151  sge0ss  47154  sge0rpcpnf  47163  sge0isum  47169  sge0xadd  47177  sge0seq  47188  ismeannd  47209  caratheodorylem1  47268  isomenndlem  47272  hoicvrrex  47298  ovn0lem  47307  hoidmvlelem2  47338  hoidmvlelem3  47339  ovnlecvr2  47352  voncmpl  47363  hspmbllem1  47368  hspmbllem2  47369  ovolval4lem1  47391  incsmf  47484  smfpimltmpt  47488  smfpimltxrmptf  47500  decsmf  47509  smfpimgtmpt  47523  smfpimgtxrmptf  47526  smfmullem1  47533  smflimsuplem2  47563  sigarac  47594  cevathlem2  47610  sin3t  47636  cos3t  47637  m1modmmod  48129  fmtnorec3  48328  fmtnorec4  48329  oddflALTV  48456  perfectALTVlem2  48515  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  uspgrlimlem1  48781  gpgvtxedg0  48856  gpgvtxedg1  48857  gpg3kgrtriexlem2  48877  ply1mulgsum  49198  lindslinindsimp2lem5  49270  nn0sumshdiglemA  49427  nn0sumshdiglemB  49428  nn0sumshdiglem2  49430  itschlc0yqe  49568