Theorem 3eqtrrd 2838

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

Syntax hints:   → wi 4   = wceq 1525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790

This theorem is referenced by:  fimacnvinrn  6712  fvcofneq  6731  iunfictbso  9393  axcnre  10439  fseq1p1m1  12835  seqf1olem1  13263  expmulz  13329  expubnd  13395  subsq  13426  bcm1k  13529  bcpasc  13535  cshwcshid  14029  crim  14312  rereb  14317  rlimrecl  14775  iseraltlem2  14877  fsumparts  14998  isumshft  15031  geoserg  15058  pwdif  15060  efsub  15290  sincossq  15366  efieq1re  15389  eucalg  15764  lcmfunsnlem  15818  phiprmpw  15946  modprmn0modprm0  15977  coprimeprodsq  15978  pythagtriplem15  15999  pythagtriplem17  16001  fldivp1  16066  1arithlem4  16095  setsidvald  16347  setsid  16371  pwsbas  16593  invfuc  17077  latdisdlem  17632  odinv  18422  frgpuplem  18629  gexexlem  18699  srgbinomlem4  18987  gsumdixp  19053  mplcoe1  19937  evlsvarsrng  19999  ply1idvr1  20148  ply1coe  20151  evls1varsrng  20189  cnfldsub  20259  mat1scmat  20836  m1detdiag  20894  mdetunilem7  20915  madugsum  20940  pm2mpmhmlem2  21115  mretopd  21388  upxp  21919  uptx  21921  imasdsf1olem  22670  clmvs2  23385  cphipipcj  23491  cphipval2  23531  itgmulc2lem2  24120  r1pid  24440  coeeulem  24501  fta1lem  24583  aaliou3lem8  24621  eff1olem  24817  tanarg  24887  logcnlem4  24913  root1cj  25022  angpieqvdlem  25091  quad2  25102  dcubic  25109  quart1  25119  jensen  25252  lgamgulmlem5  25296  lgamgulm2  25299  ftalem5  25340  basellem8  25351  chpchtsum  25481  logfaclbnd  25484  perfectlem2  25492  gausslemma2dlem1a  25627  2sqlem3  25682  dchrvmasum2lem  25758  dchrvmasumiflem2  25764  selberglem2  25808  selberg3r  25831  pntlem3  25871  ostth2  25899  ostth3  25900  krippenlem  26162  colinearalglem1  26379  axlowdimlem16  26430  axcontlem4  26440  clwlkclwwlkfo  27473  nmbdoplbi  29488  nmcopexi  29491  nmbdfnlbi  29513  nmcfnexi  29515  nmcfnlbi  29516  hstoh  29696  fcobij  30142  lt2addrd  30159  xlt2addrd  30166  cshwrnid  30305  symgfcoeu  30381  cycpmconjslem2  30431  cycpmconjs  30432  isarchi3  30450  archirngz  30452  dimkerim  30623  submatminr1  30686  mdetpmtr1  30699  madjusmdetlem1  30703  qqhnm  30844  esumfzf  30941  ddemeas  31108  sseqp1  31266  ballotlemi1  31373  ballotlemii  31374  ballotlemic  31377  ballotlem1c  31378  fsum2dsub  31491  circlemeth  31524  hgt750lemb  31540  hgt750lema  31541  hgt750leme  31542  elmrsubrn  32377  cos2h  34435  itg2addnclem  34495  itgmulc2nclem2  34511  areacirclem1  34534  areacirclem4  34537  cntotbnd  34627  atmod2i2  36550  trljat1  36854  trljat2  36855  cdleme9  36941  cdleme15b  36963  cdleme20c  36999  cdleme22eALTN  37033  dvhopN  37804  doca2N  37814  cdlemn10  37894  dochocss  38054  djhlj  38089  dihprrnlem1N  38112  dihprrnlem2  38113  lcfl7lem  38187  lclkrlem2c  38197  hgmapadd  38582  hdmapinvlem3  38608  hgmapvvlem1  38611  nn0expgcd  38727  rmydbl  39043  jm2.18  39091  jm2.19  39096  proot1hash  39306  dssmapnvod  39872  fincygsubgodd  40190  binomcxplemnotnn0  40247  oddfl  41105  dstregt0  41109  supsubc  41183  absimlere  41319  uzinico2  41401  fsumsplit1  41416  mccllem  41441  ellimcabssub0  41461  sumnnodd  41474  climresmpt  41503  limsupresuz  41547  liminfresuz  41628  coskpi2  41710  cosknegpi  41713  dvsinax  41760  dvnmptdivc  41786  dvnxpaek  41790  dvnmul  41791  dvmptfprodlem  41792  ditgeqiooicc  41808  itgioocnicc  41825  itgspltprt  41827  wallispi2lem2  41921  dirkerper  41945  dirkertrigeqlem2  41948  dirkertrigeqlem3  41949  dirkertrigeq  41950  dirkercncflem2  41953  dirkercncflem4  41955  fourierdlem18  41974  fourierdlem19  41975  fourierdlem33  41989  fourierdlem35  41991  fourierdlem41  41997  fourierdlem42  41998  fourierdlem48  42003  fourierdlem49  42004  fourierdlem50  42005  fourierdlem53  42008  fourierdlem63  42018  fourierdlem65  42020  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem81  42036  fourierdlem82  42037  fourierdlem83  42038  fourierdlem84  42039  fourierdlem90  42045  fourierdlem93  42048  fourierdlem95  42050  fourierdlem103  42058  fourierdlem104  42059  fourierdlem107  42062  fourierdlem111  42066  fourierswlem  42079  fouriersw  42080  etransclem4  42087  etransclem9  42092  etransclem28  42111  etransclem35  42118  etransclem38  42121  sge0tsms  42226  sge0sup  42237  sge0resplit  42252  sge0split  42255  sge0ss  42258  sge0rpcpnf  42267  sge0isum  42273  sge0xadd  42281  sge0seq  42292  ismeannd  42313  caratheodorylem1  42372  isomenndlem  42376  hoicvrrex  42402  ovn0lem  42411  hoidmvlelem2  42442  hoidmvlelem3  42443  ovnlecvr2  42456  voncmpl  42467  hspmbllem1  42472  hspmbllem2  42473  ovolval4lem1  42495  incsmf  42583  smfpimltmpt  42587  smfpimltxrmpt  42599  decsmf  42607  smfpimgtmpt  42621  smfpimgtxrmpt  42624  smfmullem1  42630  smfsupmpt  42653  smfinfmpt  42657  smflimsuplem2  42659  sigarac  42673  cevathlem2  42689  fmtnorec3  43214  fmtnorec4  43215  oddflALTV  43332  perfectALTVlem2  43391  nnsum4primeseven  43469  nnsum4primesevenALTV  43470  c0snmgmhm  43685  funcrngcsetc  43769  funcringcsetc  43806  ply1mulgsum  43946  lindslinindsimp2lem5  44019  m1modmmod  44084  nn0sumshdiglemA  44182  nn0sumshdiglemB  44183  nn0sumshdiglem2  44185  itschlc0yqe  44250