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 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:  fimacnvinrn  7073  fvcofneq  7094  iunfictbso  10111  axcnre  11161  fseq1p1m1  13579  seqf1olem1  14011  expmulz  14078  expubnd  14146  subsq  14178  bcm1k  14279  bcpasc  14285  cshwcshid  14782  crim  15066  rereb  15071  rlimrecl  15528  iseraltlem2  15633  fsumsplit1  15695  fsumparts  15756  isumshft  15789  geoserg  15816  pwdif  15818  efsub  16047  sincossq  16123  efieq1re  16146  eucalg  16528  lcmfunsnlem  16582  phiprmpw  16713  modprmn0modprm0  16744  coprimeprodsq  16745  pythagtriplem15  16766  pythagtriplem17  16768  fldivp1  16834  1arithlem4  16863  setsidvald  17136  setsidvaldOLD  17137  setsid  17145  pwsbas  17437  invfuc  17931  estrreslem1  18092  latdisdlem  18453  odinv  19470  frgpuplem  19681  gexexlem  19761  fincygsubgodd  20023  srgbinomlem4  20123  gsumdixp  20207  c0snmgmhm  20353  cnfldsub  21173  mplcoe1  21811  evlsvarsrng  21881  ply1idvr1  22037  ply1coe  22040  evls1varsrng  22079  mat1scmat  22261  m1detdiag  22319  mdetunilem7  22340  madugsum  22365  pm2mpmhmlem2  22541  mretopd  22816  upxp  23347  uptx  23349  imasdsf1olem  24099  clmvs2  24834  cphipipcj  24941  cphipval2  24982  itgmulc2lem2  25574  r1pid  25901  coeeulem  25962  fta1lem  26044  aaliou3lem8  26082  eff1olem  26281  tanarg  26351  logcnlem4  26377  root1cj  26488  angpieqvdlem  26557  quad2  26568  dcubic  26575  quart1  26585  jensen  26717  lgamgulmlem5  26761  lgamgulm2  26764  ftalem5  26805  basellem8  26816  chpchtsum  26946  logfaclbnd  26949  perfectlem2  26957  gausslemma2dlem1a  27092  2sqlem3  27147  dchrvmasum2lem  27223  dchrvmasumiflem2  27229  selberglem2  27273  selberg3r  27296  pntlem3  27336  ostth2  27364  ostth3  27365  madeoldsuc  27604  krippenlem  28196  colinearalglem1  28419  axlowdimlem16  28470  axcontlem4  28480  clwlkclwwlkfo  29517  nmbdoplbi  31532  nmcopexi  31535  nmbdfnlbi  31557  nmcfnexi  31559  nmcfnlbi  31560  hstoh  31740  fcobij  32202  lt2addrd  32219  xlt2addrd  32226  cshwrnid  32380  symgfcoeu  32501  cycpmconjslem2  32572  cycpmconjs  32573  isarchi3  32591  archirngz  32593  ghmquskerco  32791  elrspunsn  32809  mxidlirredi  32849  dimkerim  32988  submatminr1  33076  mdetpmtr1  33089  madjusmdetlem1  33093  zarcmplem  33147  qqhnm  33256  esumfzf  33353  ddemeas  33520  sseqp1  33680  ballotlemi1  33787  ballotlemii  33788  ballotlemic  33791  ballotlem1c  33792  fsum2dsub  33905  circlemeth  33938  hgt750lemb  33954  hgt750lema  33955  hgt750leme  33956  elmrsubrn  34797  cos2h  36782  itg2addnclem  36842  itgmulc2nclem2  36858  areacirclem1  36879  areacirclem4  36882  cntotbnd  36967  atmod2i2  39036  trljat1  39340  trljat2  39341  cdleme9  39427  cdleme15b  39449  cdleme20c  39485  cdleme22eALTN  39519  dvhopN  40290  doca2N  40300  cdlemn10  40380  dochocss  40540  djhlj  40575  dihprrnlem1N  40598  dihprrnlem2  40599  lcfl7lem  40673  lclkrlem2c  40683  hgmapadd  41068  hdmapinvlem3  41094  hgmapvvlem1  41097  selvvvval  41459  sumcubes  41513  nn0expgcd  41528  zaddcomlem  41626  rmydbl  41981  jm2.18  42029  jm2.19  42034  proot1hash  42244  dssmapnvod  43073  binomcxplemnotnn0  43417  oddfl  44286  dstregt0  44290  supsubc  44362  absimlere  44489  uzinico2  44574  mccllem  44612  ellimcabssub0  44632  sumnnodd  44645  climresmpt  44674  limsupresuz  44718  liminfresuz  44799  coskpi2  44881  cosknegpi  44884  dvsinax  44928  dvnmptdivc  44953  dvnxpaek  44957  dvnmul  44958  dvmptfprodlem  44959  ditgeqiooicc  44975  itgioocnicc  44992  itgspltprt  44994  wallispi2lem2  45087  dirkerper  45111  dirkertrigeqlem2  45114  dirkertrigeqlem3  45115  dirkertrigeq  45116  dirkercncflem2  45119  dirkercncflem4  45121  fourierdlem18  45140  fourierdlem19  45141  fourierdlem33  45155  fourierdlem35  45157  fourierdlem41  45163  fourierdlem42  45164  fourierdlem48  45169  fourierdlem49  45170  fourierdlem50  45171  fourierdlem53  45174  fourierdlem63  45184  fourierdlem65  45186  fourierdlem73  45194  fourierdlem74  45195  fourierdlem75  45196  fourierdlem81  45202  fourierdlem82  45203  fourierdlem83  45204  fourierdlem84  45205  fourierdlem90  45211  fourierdlem93  45214  fourierdlem95  45216  fourierdlem103  45224  fourierdlem104  45225  fourierdlem107  45228  fourierdlem111  45232  fourierswlem  45245  fouriersw  45246  etransclem4  45253  etransclem9  45258  etransclem28  45277  etransclem35  45284  etransclem38  45287  sge0tsms  45395  sge0sup  45406  sge0resplit  45421  sge0split  45424  sge0ss  45427  sge0rpcpnf  45436  sge0isum  45442  sge0xadd  45450  sge0seq  45461  ismeannd  45482  caratheodorylem1  45541  isomenndlem  45545  hoicvrrex  45571  ovn0lem  45580  hoidmvlelem2  45611  hoidmvlelem3  45612  ovnlecvr2  45625  voncmpl  45636  hspmbllem1  45641  hspmbllem2  45642  ovolval4lem1  45664  incsmf  45757  smfpimltmpt  45761  smfpimltxrmptf  45773  decsmf  45782  smfpimgtmpt  45796  smfpimgtxrmptf  45799  smfmullem1  45806  smfinfmpt  45834  smflimsuplem2  45836  sigarac  45867  cevathlem2  45883  fmtnorec3  46515  fmtnorec4  46516  oddflALTV  46630  perfectALTVlem2  46689  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  funcrngcsetc  46985  funcringcsetc  47022  ply1mulgsum  47159  lindslinindsimp2lem5  47231  m1modmmod  47295  nn0sumshdiglemA  47393  nn0sumshdiglemB  47394  nn0sumshdiglem2  47396  itschlc0yqe  47534