Theorem 3eqtrrd 2777

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 2772	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2773	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  fimacnvinrn  7018  fvcofneq  7040  iunfictbso  10030  axcnre  11081  fseq1p1m1  13546  seqf1olem1  13997  expmulz  14064  expubnd  14134  subsq  14166  bcm1k  14271  bcpasc  14277  cshwcshid  14783  crim  15071  rereb  15076  rlimrecl  15536  iseraltlem2  15639  fsumsplit1  15701  fsumparts  15763  isumshft  15798  geoserg  15825  pwdif  15827  efsub  16061  sincossq  16137  efieq1re  16160  nn0expgcd  16527  eucalg  16550  lcmfunsnlem  16604  phiprmpw  16740  modprmn0modprm0  16772  coprimeprodsq  16773  pythagtriplem15  16794  pythagtriplem17  16796  fldivp1  16862  1arithlem4  16891  setsidvald  17163  setsid  17171  pwsbas  17444  invfuc  17938  estrreslem1  18097  latdisdlem  18456  ghmquskerco  19253  odinv  19530  frgpuplem  19741  gexexlem  19821  fincygsubgodd  20083  srgbinomlem4  20204  gsumdixp  20292  c0snmgmhm  20436  funcrngcsetc  20611  funcringcsetc  20645  cnfldsub  21390  mplcoe1  22028  evlsvarsrng  22098  psdmul  22145  ply1idvr1OLD  22273  ply1coe  22276  evls1varsrng  22318  mat1scmat  22517  m1detdiag  22575  mdetunilem7  22596  madugsum  22621  pm2mpmhmlem2  22797  mretopd  23070  upxp  23601  uptx  23603  imasdsf1olem  24351  clmvs2  25074  cphipipcj  25180  cphipval2  25221  itgmulc2lem2  25813  r1pid  26139  coeeulem  26202  fta1lem  26287  aaliou3lem8  26325  eff1olem  26528  tanarg  26599  logcnlem4  26625  root1cj  26736  angpieqvdlem  26808  quad2  26819  dcubic  26826  quart1  26836  jensen  26969  lgamgulmlem5  27013  lgamgulm2  27016  ftalem5  27057  basellem8  27068  chpchtsum  27199  logfaclbnd  27202  perfectlem2  27210  gausslemma2dlem1a  27345  2sqlem3  27400  dchrvmasum2lem  27476  dchrvmasumiflem2  27482  selberglem2  27526  selberg3r  27549  pntlem3  27589  ostth2  27617  ostth3  27618  madeoldsuc  27894  zseo  28431  addhalfcut  28468  pw2cut2  28471  krippenlem  28775  colinearalglem1  28992  axlowdimlem16  29043  axcontlem4  29053  clwlkclwwlkfo  30097  nmbdoplbi  32113  nmcopexi  32116  nmbdfnlbi  32138  nmcfnexi  32140  nmcfnlbi  32141  hstoh  32321  fcobij  32811  lt2addrd  32841  xlt2addrd  32850  cshwrnid  33039  symgfcoeu  33161  cycpmconjslem2  33234  cycpmconjs  33235  isarchi3  33266  archirngz  33268  elrgspnsubrunlem1  33326  elrspunsn  33507  mxidlirredi  33549  1arithidomlem1  33613  1arithidomlem2  33614  1arithidom  33615  evlextv  33704  esplyfval1  33735  dimkerim  33790  lvecendof1f1o  33796  fldextrspunlsplem  33836  nn0constr  33924  constraddcl  33925  constrnegcl  33926  constrremulcl  33930  constrrecl  33932  constrimcl  33933  constrmulcl  33934  constrreinvcl  33935  constrinvcl  33936  constrresqrtcl  33940  constrabscl  33941  2sqr3minply  33943  submatminr1  33973  mdetpmtr1  33986  madjusmdetlem1  33990  zarcmplem  34044  qqhnm  34153  esumfzf  34232  ddemeas  34399  sseqp1  34558  ballotlemi1  34666  ballotlemii  34667  ballotlemic  34670  ballotlem1c  34671  fsum2dsub  34770  circlemeth  34803  hgt750lemb  34819  hgt750lema  34820  hgt750leme  34821  elmrsubrn  35721  cos2h  37949  itg2addnclem  38009  itgmulc2nclem2  38025  areacirclem1  38046  areacirclem4  38049  cntotbnd  38134  atmod2i2  40325  trljat1  40629  trljat2  40630  cdleme9  40716  cdleme15b  40738  cdleme20c  40774  cdleme22eALTN  40808  dvhopN  41579  doca2N  41589  cdlemn10  41669  dochocss  41829  djhlj  41864  dihprrnlem1N  41887  dihprrnlem2  41888  lcfl7lem  41962  lclkrlem2c  41972  hgmapadd  42357  hdmapinvlem3  42383  hgmapvvlem1  42386  sumcubes  42762  zaddcomlem  42925  fidomncyc  42997  selvvvval  43035  rmydbl  43389  jm2.18  43437  jm2.19  43442  proot1hash  43644  dssmapnvod  44468  binomcxplemnotnn0  44804  oddfl  45732  dstregt0  45736  supsubc  45804  absimlere  45928  uzinico2  46012  mccllem  46048  ellimcabssub0  46068  sumnnodd  46081  climresmpt  46108  limsupresuz  46152  liminfresuz  46233  coskpi2  46315  cosknegpi  46318  dvsinax  46362  dvnmptdivc  46387  dvnxpaek  46391  dvnmul  46392  dvmptfprodlem  46393  ditgeqiooicc  46409  itgioocnicc  46426  itgspltprt  46428  wallispi2lem2  46521  dirkerper  46545  dirkertrigeqlem2  46548  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem18  46574  fourierdlem19  46575  fourierdlem33  46589  fourierdlem35  46591  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem53  46608  fourierdlem63  46618  fourierdlem65  46620  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem81  46636  fourierdlem82  46637  fourierdlem83  46638  fourierdlem84  46639  fourierdlem90  46645  fourierdlem93  46648  fourierdlem95  46650  fourierdlem103  46658  fourierdlem104  46659  fourierdlem107  46662  fourierdlem111  46666  fourierswlem  46679  fouriersw  46680  etransclem4  46687  etransclem9  46692  etransclem28  46711  etransclem35  46718  etransclem38  46721  sge0tsms  46829  sge0sup  46840  sge0resplit  46855  sge0split  46858  sge0ss  46861  sge0rpcpnf  46870  sge0isum  46876  sge0xadd  46884  sge0seq  46895  ismeannd  46916  caratheodorylem1  46975  isomenndlem  46979  hoicvrrex  47005  ovn0lem  47014  hoidmvlelem2  47045  hoidmvlelem3  47046  ovnlecvr2  47059  voncmpl  47070  hspmbllem1  47075  hspmbllem2  47076  ovolval4lem1  47098  incsmf  47191  smfpimltmpt  47195  smfpimltxrmptf  47207  decsmf  47216  smfpimgtmpt  47230  smfpimgtxrmptf  47233  smfmullem1  47240  smflimsuplem2  47270  sigarac  47301  cevathlem2  47317  sin3t  47338  cos3t  47339  m1modmmod  47827  fmtnorec3  48026  fmtnorec4  48027  oddflALTV  48154  perfectALTVlem2  48213  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  uspgrlimlem1  48479  gpgvtxedg0  48554  gpgvtxedg1  48555  gpg3kgrtriexlem2  48575  ply1mulgsum  48881  lindslinindsimp2lem5  48953  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem2  49113  itschlc0yqe  49251