Theorem 3eqtrrd 2783

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  fimacnvinrn  6931  fvcofneq  6951  iunfictbso  9801  axcnre  10851  fseq1p1m1  13259  seqf1olem1  13690  expmulz  13757  expubnd  13823  subsq  13854  bcm1k  13957  bcpasc  13963  cshwcshid  14468  crim  14754  rereb  14759  rlimrecl  15217  iseraltlem2  15322  fsumsplit1  15385  fsumparts  15446  isumshft  15479  geoserg  15506  pwdif  15508  efsub  15737  sincossq  15813  efieq1re  15836  eucalg  16220  lcmfunsnlem  16274  phiprmpw  16405  modprmn0modprm0  16436  coprimeprodsq  16437  pythagtriplem15  16458  pythagtriplem17  16460  fldivp1  16526  1arithlem4  16555  setsidvald  16828  setsidvaldOLD  16829  setsid  16837  pwsbas  17115  invfuc  17608  estrreslem1  17769  latdisdlem  18129  odinv  19083  frgpuplem  19293  gexexlem  19368  fincygsubgodd  19630  srgbinomlem4  19694  gsumdixp  19763  cnfldsub  20538  mplcoe1  21148  evlsvarsrng  21219  ply1idvr1  21374  ply1coe  21377  evls1varsrng  21416  mat1scmat  21596  m1detdiag  21654  mdetunilem7  21675  madugsum  21700  pm2mpmhmlem2  21876  mretopd  22151  upxp  22682  uptx  22684  imasdsf1olem  23434  clmvs2  24163  cphipipcj  24269  cphipval2  24310  itgmulc2lem2  24902  r1pid  25229  coeeulem  25290  fta1lem  25372  aaliou3lem8  25410  eff1olem  25609  tanarg  25679  logcnlem4  25705  root1cj  25814  angpieqvdlem  25883  quad2  25894  dcubic  25901  quart1  25911  jensen  26043  lgamgulmlem5  26087  lgamgulm2  26090  ftalem5  26131  basellem8  26142  chpchtsum  26272  logfaclbnd  26275  perfectlem2  26283  gausslemma2dlem1a  26418  2sqlem3  26473  dchrvmasum2lem  26549  dchrvmasumiflem2  26555  selberglem2  26599  selberg3r  26622  pntlem3  26662  ostth2  26690  ostth3  26691  krippenlem  26955  colinearalglem1  27177  axlowdimlem16  27228  axcontlem4  27238  clwlkclwwlkfo  28274  nmbdoplbi  30287  nmcopexi  30290  nmbdfnlbi  30312  nmcfnexi  30314  nmcfnlbi  30315  hstoh  30495  fcobij  30959  lt2addrd  30976  xlt2addrd  30983  cshwrnid  31135  symgfcoeu  31253  cycpmconjslem2  31324  cycpmconjs  31325  isarchi3  31343  archirngz  31345  dimkerim  31610  submatminr1  31662  mdetpmtr1  31675  madjusmdetlem1  31679  zarcmplem  31733  qqhnm  31840  esumfzf  31937  ddemeas  32104  sseqp1  32262  ballotlemi1  32369  ballotlemii  32370  ballotlemic  32373  ballotlem1c  32374  fsum2dsub  32487  circlemeth  32520  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  elmrsubrn  33382  madeoldsuc  33994  cos2h  35695  itg2addnclem  35755  itgmulc2nclem2  35771  areacirclem1  35792  areacirclem4  35795  cntotbnd  35881  atmod2i2  37803  trljat1  38107  trljat2  38108  cdleme9  38194  cdleme15b  38216  cdleme20c  38252  cdleme22eALTN  38286  dvhopN  39057  doca2N  39067  cdlemn10  39147  dochocss  39307  djhlj  39342  dihprrnlem1N  39365  dihprrnlem2  39366  lcfl7lem  39440  lclkrlem2c  39450  hgmapadd  39835  hdmapinvlem3  39861  hgmapvvlem1  39864  mhphf  40208  nn0expgcd  40256  rmydbl  40678  jm2.18  40726  jm2.19  40731  proot1hash  40941  dssmapnvod  41517  binomcxplemnotnn0  41863  oddfl  42705  dstregt0  42709  supsubc  42782  absimlere  42910  uzinico2  42990  mccllem  43028  ellimcabssub0  43048  sumnnodd  43061  climresmpt  43090  limsupresuz  43134  liminfresuz  43215  coskpi2  43297  cosknegpi  43300  dvsinax  43344  dvnmptdivc  43369  dvnxpaek  43373  dvnmul  43374  dvmptfprodlem  43375  ditgeqiooicc  43391  itgioocnicc  43408  itgspltprt  43410  wallispi2lem2  43503  dirkerper  43527  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem18  43556  fourierdlem19  43557  fourierdlem33  43571  fourierdlem35  43573  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem53  43590  fourierdlem63  43600  fourierdlem65  43602  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem84  43621  fourierdlem90  43627  fourierdlem93  43630  fourierdlem95  43632  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierswlem  43661  fouriersw  43662  etransclem4  43669  etransclem9  43674  etransclem28  43693  etransclem35  43700  etransclem38  43703  sge0tsms  43808  sge0sup  43819  sge0resplit  43834  sge0split  43837  sge0ss  43840  sge0rpcpnf  43849  sge0isum  43855  sge0xadd  43863  sge0seq  43874  ismeannd  43895  caratheodorylem1  43954  isomenndlem  43958  hoicvrrex  43984  ovn0lem  43993  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnlecvr2  44038  voncmpl  44049  hspmbllem1  44054  hspmbllem2  44055  ovolval4lem1  44077  incsmf  44165  smfpimltmpt  44169  smfpimltxrmpt  44181  decsmf  44189  smfpimgtmpt  44203  smfpimgtxrmpt  44206  smfmullem1  44212  smfinfmpt  44239  smflimsuplem2  44241  sigarac  44255  cevathlem2  44271  fmtnorec3  44888  fmtnorec4  44889  oddflALTV  45003  perfectALTVlem2  45062  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  c0snmgmhm  45360  funcrngcsetc  45444  funcringcsetc  45481  ply1mulgsum  45619  lindslinindsimp2lem5  45691  m1modmmod  45755  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdiglem2  45856  itschlc0yqe  45994