Theorem 3eqtrrd 2805

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

This proof depends on syntax axioms:   → wi 4   = 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 2156  ax-ext 2737

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

This theorem is used by:  fimacnvinrn  7070  fvcofneq  7092  iunfictbso  10114  axcnre  11166  fseq1p1m1  13645  seqf1olem1  14097  expmulz  14164  expubnd  14234  subsq  14266  bcm1k  14371  bcpasc  14377  cshwcshid  14890  crim  15192  rereb  15197  rlimrecl  15657  iseraltlem2  15760  fsumsplit1  15821  fsumparts  15883  isumshft  15918  geoserg  15945  pwdif  15947  efsub  16180  sincossq  16256  efieq1re  16279  nn0expgcd  16646  eucalg  16669  lcmfunsnlem  16723  phiprmpw  16859  modprmn0modprm0  16891  coprimeprodsq  16892  pythagtriplem15  16913  pythagtriplem17  16915  fldivp1  16981  1arithlem4  17010  setsidvald  17283  setsid  17291  pwsbas  17564  invfuc  18058  estrreslem1  18217  latdisdlem  18576  ghmquskerco  19400  odinv  19677  frgpuplem  19888  gexexlem  19968  fincygsubgodd  20230  srgbinomlem4  20357  gsumdixp  20448  c0snmgmhm  20592  funcrngcsetc  20791  funcringcsetc  20825  cnfldsub  21602  mplcoe1  22240  evlsvarsrng  22310  selvvvval  22345  psdmul  22381  ply1coe  22510  evls1varsrng  22552  mat1scmat  22748  m1detdiag  22806  mdetunilem7  22827  madugsum  22852  pm2mpmhmlem2  23028  mretopd  23301  upxp  23833  uptx  23835  imasdsf1olem  24583  clmvs2  25306  cphipipcj  25412  cphipval2  25453  itgmulc2lem2  26045  r1pid  26371  coeeulem  26434  fta1lem  26521  aaliou3lem8  26561  eff1olem  26766  tanarg  26837  logcnlem4  26863  root1cj  26974  angpieqvdlem  27046  quad2  27057  dcubic  27064  quart1  27074  jensen  27206  lgamgulmlem5  27250  lgamgulm2  27253  ftalem5  27294  basellem8  27305  chpchtsum  27436  logfaclbnd  27439  perfectlem2  27447  gausslemma2dlem1a  27582  2sqlem3  27637  dchrvmasum2lem  27713  dchrvmasumiflem2  27719  selberglem2  27763  selberg3r  27786  pntlem3  27826  ostth2  27854  ostth3  27855  madeoldsuc  28131  zseo  28668  addhalfcut  28705  pw2cut2  28708  krippenlem  29020  colinearalglem1  29313  axlowdimlem16  29364  axcontlem4  29374  clwlkclwwlkfo  30429  nmbdoplbi  32449  nmcopexi  32452  nmbdfnlbi  32474  nmcfnexi  32476  nmcfnlbi  32477  hstoh  32657  fcobij  33137  lt2addrd  33167  xlt2addrd  33176  cshwrnid  33347  symgfcoeu  33468  cycpmconjslem2  33541  cycpmconjs  33542  isarchi3  33573  archirngz  33575  elrgspnsubrunlem1  33633  elrspunsn  33803  mxidlirredi  33820  1arithidomlem1  33891  1arithidomlem2  33892  1arithidom  33893  evlextv  33998  esplyfval1  34029  dimkerim  34083  lvecendof1f1o  34089  fldextrspunlsplem  34129  nn0constr  34217  constraddcl  34218  constrnegcl  34219  constrremulcl  34223  constrrecl  34225  constrimcl  34226  constrmulcl  34227  constrreinvcl  34228  constrinvcl  34229  constrresqrtcl  34233  constrabscl  34234  2sqr3minply  34236  submatminr1  34266  mdetpmtr1  34279  madjusmdetlem1  34283  zarcmplem  34337  qqhnm  34446  esumfzf  34525  ddemeas  34693  sseqp1  34852  ballotlemi1  34960  ballotlemii  34961  ballotlemic  34964  ballotlem1c  34965  fsum2dsub  35061  circlemeth  35094  hgt750lemb  35110  hgt750lema  35111  hgt750leme  35112  elmrsubrn  36051  nadddilem1  36751  cos2h  38321  itg2addnclem  38381  itgmulc2nclem2  38397  areacirclem1  38418  areacirclem4  38421  cntotbnd  38507  atmod2i2  40696  trljat1  41000  trljat2  41001  cdleme9  41087  cdleme15b  41109  cdleme20c  41145  cdleme22eALTN  41179  dvhopN  41950  doca2N  41960  cdlemn10  42040  dochocss  42200  djhlj  42235  dihprrnlem1N  42258  dihprrnlem2  42259  lcfl7lem  42333  lclkrlem2c  42343  hgmapadd  42728  hdmapinvlem3  42754  hgmapvvlem1  42757  sumcubes  43134  zaddcomlem  43297  fidomncyc  43363  rmydbl  43727  jm2.18  43775  jm2.19  43780  proot1hash  43982  dssmapnvod  44806  binomcxplemnotnn0  45126  oddfl  46057  dstregt0  46061  supsubc  46129  absimlere  46253  uzinico2  46337  mccllem  46373  ellimcabssub0  46393  sumnnodd  46406  climresmpt  46433  limsupresuz  46477  liminfresuz  46558  coskpi2  46640  cosknegpi  46643  dvsinax  46687  dvnmptdivc  46712  dvnxpaek  46716  dvnmul  46717  dvmptfprodlem  46718  ditgeqiooicc  46734  itgioocnicc  46751  itgspltprt  46753  wallispi2lem2  46846  dirkerper  46870  dirkertrigeqlem2  46873  dirkertrigeqlem3  46874  dirkertrigeq  46875  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem18  46899  fourierdlem19  46900  fourierdlem33  46914  fourierdlem35  46916  fourierdlem41  46922  fourierdlem42  46923  fourierdlem48  46928  fourierdlem49  46929  fourierdlem50  46930  fourierdlem53  46933  fourierdlem63  46943  fourierdlem65  46945  fourierdlem73  46953  fourierdlem74  46954  fourierdlem75  46955  fourierdlem81  46961  fourierdlem82  46962  fourierdlem83  46963  fourierdlem84  46964  fourierdlem90  46970  fourierdlem93  46973  fourierdlem95  46975  fourierdlem103  46983  fourierdlem104  46984  fourierdlem107  46987  fourierdlem111  46991  fourierswlem  47004  fouriersw  47005  etransclem4  47012  etransclem9  47017  etransclem28  47036  etransclem35  47043  etransclem38  47046  sge0tsms  47154  sge0sup  47165  sge0resplit  47180  sge0split  47183  sge0ss  47186  sge0rpcpnf  47195  sge0isum  47201  sge0xadd  47209  sge0seq  47220  ismeannd  47241  caratheodorylem1  47300  isomenndlem  47304  hoicvrrex  47330  ovn0lem  47339  hoidmvlelem2  47370  hoidmvlelem3  47371  ovnlecvr2  47384  voncmpl  47395  hspmbllem1  47400  hspmbllem2  47401  ovolval4lem1  47423  incsmf  47516  smfpimltmpt  47520  smfpimltxrmptf  47532  decsmf  47541  smfpimgtmpt  47555  smfpimgtxrmptf  47558  smfmullem1  47565  smflimsuplem2  47595  sigarac  47626  cevathlem2  47642  sin3t  47668  cos3t  47669  m1modmmod  48161  fmtnorec3  48360  fmtnorec4  48361  oddflALTV  48488  perfectALTVlem2  48547  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  uspgrlimlem1  48813  gpgvtxedg0  48888  gpgvtxedg1  48889  gpg3kgrtriexlem2  48909  ply1mulgsum  49229  lindslinindsimp2lem5  49301  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdiglem2  49461  itschlc0yqe  49599