Theorem 3eqtrrd 2803

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 2798	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2799	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  fimacnvinrn  7103  fvcofneq  7125  iunfictbso  10232  axcnre  11288  fseq1p1m1  13772  seqf1olem1  14224  expmulz  14291  expubnd  14361  subsq  14394  bcm1k  14500  bcpasc  14506  cshwcshid  15020  crim  15325  rereb  15330  rlimrecl  15791  iseraltlem2  15894  fsumsplit1  15955  fsumparts  16017  isumshft  16052  geoserg  16079  pwdif  16081  efsub  16312  sincossq  16388  efieq1re  16411  nn0expgcd  16782  eucalg  16806  lcmfunsnlem  16860  phiprmpw  16997  modprmn0modprm0  17029  coprimeprodsq  17030  pythagtriplem15  17051  pythagtriplem17  17053  fldivp1  17119  1arithlem4  17148  setsidvald  17421  setsid  17429  pwsbas  17708  invfuc  18202  estrreslem1  18361  latdisdlem  18720  ghmquskerco  19549  odinv  19826  frgpuplem  20037  gexexlem  20117  fincygsubgodd  20379  srgbinomlem4  20506  gsumdixp  20599  c0snmgmhm  20743  funcrngcsetc  20943  funcringcsetc  20977  cnfldsub  21758  mplcoe1  22401  evlsvarsrng  22471  selvvvval  22506  psdmul  22542  ply1coe  22671  evls1varsrng  22713  mat1scmat  22909  m1detdiag  22967  mdetunilem7  22988  madugsum  23013  pm2mpmhmlem2  23192  mretopd  23465  upxp  23997  uptx  23999  imasdsf1olem  24747  clmvs2  25470  cphipipcj  25576  cphipval2  25617  itgmulc2lem2  26208  r1pid  26534  coeeulem  26598  fta1lem  26683  aaliou3lem8  26729  eff1olem  26933  tanarg  27004  logcnlem4  27030  root1cj  27141  angpieqvdlem  27213  quad2  27224  dcubic  27231  quart1  27241  jensen  27373  lgamgulmlem5  27417  lgamgulm2  27420  ftalem5  27461  basellem8  27472  chpchtsum  27603  logfaclbnd  27606  perfectlem2  27614  gausslemma2dlem1a  27749  2sqlem3  27804  dchrvmasum2lem  27880  dchrvmasumiflem2  27886  selberglem2  27930  selberg3r  27953  pntlem3  27993  ostth2  28021  ostth3  28022  madeoldsuc  28328  zseo  28865  addhalfcut  28902  pw2cut2  28905  krippenlem  29219  colinearalglem1  29541  axlowdimlem16  29592  axcontlem4  29602  clwlkclwwlkfo  30657  nmbdoplbi  32683  nmcopexi  32686  nmbdfnlbi  32708  nmcfnexi  32710  nmcfnlbi  32711  hstoh  32891  fcobij  33408  lt2addrd  33438  xlt2addrd  33447  cshwrnid  33618  symgfcoeu  33742  cycpmconjslem2  33815  cycpmconjs  33816  isarchi3  33847  archirngz  33849  elrgspnsubrunlem1  33907  fldedom  33956  elrspunsn  34083  mxidlirredi  34100  1arithidomlem1  34171  1arithidomlem2  34172  1arithidom  34173  rngunsnply1  34249  evlextv  34285  esplyfval1  34316  dimkerim  34370  lvecendof1f1o  34376  fldextrspunlsplem  34416  nn0constr  34504  constraddcl  34505  constrnegcl  34506  constrremulcl  34510  constrrecl  34512  constrimcl  34513  constrmulcl  34514  constrreinvcl  34515  constrinvcl  34516  constrresqrtcl  34520  constrabscl  34521  2sqr3minply  34523  submatminr1  34553  mdetpmtr1  34566  madjusmdetlem1  34570  zarcmplem  34624  qqhnm  34733  esumfzf  34812  ddemeas  34980  sseqp1  35138  ballotlemi1  35246  ballotlemii  35247  ballotlemic  35250  ballotlem1c  35251  fsum2dsub  35347  circlemeth  35380  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  elmrsubrn  36493  nadddilem1  37184  cos2h  38802  itg2addnclem  38857  itgmulc2nclem2  38873  areacirclem1  38894  areacirclem4  38897  cntotbnd  38996  atmod2i2  41185  trljat1  41489  trljat2  41490  cdleme9  41576  cdleme15b  41598  cdleme20c  41634  cdleme22eALTN  41668  dvhopN  42439  doca2N  42449  cdlemn10  42529  dochocss  42689  djhlj  42724  dihprrnlem1N  42747  dihprrnlem2  42748  lcfl7lem  42822  lclkrlem2c  42832  hgmapadd  43217  hdmapinvlem3  43243  hgmapvvlem1  43246  sumcubes  43636  zaddcomlem  43793  fidomncyc  43865  rmydbl  44213  jm2.18  44261  jm2.19  44266  proot1hash  44458  dssmapnvod  45281  binomcxplemnotnn0  45601  oddfl  46567  dstregt0  46571  supsubc  46638  absimlere  46762  uzinico2  46846  mccllem  46882  ellimcabssub0  46902  sumnnodd  46915  climresmpt  46942  limsupresuz  46986  liminfresuz  47067  coskpi2  47149  cosknegpi  47152  dvsinax  47196  dvnmptdivc  47221  dvnxpaek  47225  dvnmul  47226  dvmptfprodlem  47227  ditgeqiooicc  47243  itgioocnicc  47260  itgspltprt  47262  wallispi2lem2  47355  dirkerper  47379  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkertrigeq  47384  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem18  47408  fourierdlem19  47409  fourierdlem33  47423  fourierdlem35  47425  fourierdlem41  47431  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem53  47442  fourierdlem63  47452  fourierdlem65  47454  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem81  47470  fourierdlem82  47471  fourierdlem83  47472  fourierdlem84  47473  fourierdlem90  47479  fourierdlem93  47482  fourierdlem95  47484  fourierdlem103  47492  fourierdlem104  47493  fourierdlem107  47496  fourierdlem111  47500  fourierswlem  47513  fouriersw  47514  etransclem4  47521  etransclem9  47526  etransclem28  47545  etransclem35  47552  etransclem38  47555  sge0tsms  47663  sge0sup  47674  sge0resplit  47689  sge0split  47692  sge0ss  47695  sge0rpcpnf  47704  sge0isum  47710  sge0xadd  47718  sge0seq  47729  ismeannd  47750  caratheodorylem1  47809  isomenndlem  47813  hoicvrrex  47839  ovn0lem  47848  hoidmvlelem2  47879  hoidmvlelem3  47880  ovnlecvr2  47893  voncmpl  47904  hspmbllem1  47909  hspmbllem2  47910  ovolval4lem1  47932  incsmf  48025  smfpimltmpt  48029  smfpimltxrmptf  48041  decsmf  48050  smfpimgtmpt  48064  smfpimgtxrmptf  48067  smfmullem1  48074  smflimsuplem2  48104  sigarac  48135  cevathlem2  48151  sin3t  48190  cos3t  48191  m1modmmod  48707  fmtnorec3  48906  fmtnorec4  48907  oddflALTV  49034  perfectALTVlem2  49093  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  uspgrlimlem1  49359  gpgvtxedg0  49434  gpgvtxedg1  49435  gpg3kgrtriexlem2  49455  ply1mulgsum  49833  lindslinindsimp2lem5  49905  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdiglem2  50065  itschlc0yqe  50203