Theorem 3eqtrrd 2802

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  fimacnvinrn  7052  fvcofneq  7074  iunfictbso  10070  axcnre  11122  fseq1p1m1  13603  seqf1olem1  14054  expmulz  14121  expubnd  14191  subsq  14223  bcm1k  14328  bcpasc  14334  cshwcshid  14840  crim  15142  rereb  15147  rlimrecl  15607  iseraltlem2  15710  fsumsplit1  15772  fsumparts  15834  isumshft  15869  geoserg  15896  pwdif  15898  efsub  16132  sincossq  16208  efieq1re  16231  nn0expgcd  16598  eucalg  16621  lcmfunsnlem  16675  phiprmpw  16811  modprmn0modprm0  16843  coprimeprodsq  16844  pythagtriplem15  16865  pythagtriplem17  16867  fldivp1  16933  1arithlem4  16962  setsidvald  17235  setsid  17243  pwsbas  17516  invfuc  18010  estrreslem1  18169  latdisdlem  18528  ghmquskerco  19324  odinv  19601  frgpuplem  19812  gexexlem  19892  fincygsubgodd  20154  srgbinomlem4  20279  gsumdixp  20367  c0snmgmhm  20511  funcrngcsetc  20690  funcringcsetc  20724  cnfldsub  21452  mplcoe1  22090  evlsvarsrng  22160  selvvvval  22195  psdmul  22231  ply1idvr1OLD  22358  ply1coe  22361  evls1varsrng  22403  mat1scmat  22599  m1detdiag  22657  mdetunilem7  22678  madugsum  22703  pm2mpmhmlem2  22879  mretopd  23152  upxp  23683  uptx  23685  imasdsf1olem  24433  clmvs2  25156  cphipipcj  25262  cphipval2  25303  itgmulc2lem2  25895  r1pid  26221  coeeulem  26284  fta1lem  26371  aaliou3lem8  26409  eff1olem  26613  tanarg  26684  logcnlem4  26710  root1cj  26821  angpieqvdlem  26893  quad2  26904  dcubic  26911  quart1  26921  jensen  27053  lgamgulmlem5  27097  lgamgulm2  27100  ftalem5  27141  basellem8  27152  chpchtsum  27283  logfaclbnd  27286  perfectlem2  27294  gausslemma2dlem1a  27429  2sqlem3  27484  dchrvmasum2lem  27560  dchrvmasumiflem2  27566  selberglem2  27610  selberg3r  27633  pntlem3  27673  ostth2  27701  ostth3  27702  madeoldsuc  27978  zseo  28515  addhalfcut  28552  pw2cut2  28555  krippenlem  28863  colinearalglem1  29107  axlowdimlem16  29158  axcontlem4  29168  clwlkclwwlkfo  30211  nmbdoplbi  32227  nmcopexi  32230  nmbdfnlbi  32252  nmcfnexi  32254  nmcfnlbi  32255  hstoh  32435  fcobij  32922  lt2addrd  32952  xlt2addrd  32961  cshwrnid  33139  symgfcoeu  33262  cycpmconjslem2  33335  cycpmconjs  33336  isarchi3  33367  archirngz  33369  elrgspnsubrunlem1  33428  elrspunsn  33615  mxidlirredi  33659  1arithidomlem1  33731  1arithidomlem2  33732  1arithidom  33733  evlextv  33839  esplyfval1  33870  dimkerim  33924  lvecendof1f1o  33930  fldextrspunlsplem  33970  nn0constr  34058  constraddcl  34059  constrnegcl  34060  constrremulcl  34064  constrrecl  34066  constrimcl  34067  constrmulcl  34068  constrreinvcl  34069  constrinvcl  34070  constrresqrtcl  34074  constrabscl  34075  2sqr3minply  34077  submatminr1  34107  mdetpmtr1  34120  madjusmdetlem1  34124  zarcmplem  34178  qqhnm  34287  esumfzf  34366  ddemeas  34533  sseqp1  34692  ballotlemi1  34800  ballotlemii  34801  ballotlemic  34804  ballotlem1c  34805  fsum2dsub  34901  circlemeth  34934  hgt750lemb  34950  hgt750lema  34951  hgt750leme  34952  elmrsubrn  35870  cos2h  38110  itg2addnclem  38170  itgmulc2nclem2  38186  areacirclem1  38207  areacirclem4  38210  cntotbnd  38295  atmod2i2  40486  trljat1  40790  trljat2  40791  cdleme9  40877  cdleme15b  40899  cdleme20c  40935  cdleme22eALTN  40969  dvhopN  41740  doca2N  41750  cdlemn10  41830  dochocss  41990  djhlj  42025  dihprrnlem1N  42048  dihprrnlem2  42049  lcfl7lem  42123  lclkrlem2c  42133  hgmapadd  42518  hdmapinvlem3  42544  hgmapvvlem1  42547  sumcubes  42922  zaddcomlem  43085  fidomncyc  43153  rmydbl  43517  jm2.18  43565  jm2.19  43570  proot1hash  43772  dssmapnvod  44596  binomcxplemnotnn0  44932  oddfl  45857  dstregt0  45861  supsubc  45929  absimlere  46053  uzinico2  46137  mccllem  46173  ellimcabssub0  46193  sumnnodd  46206  climresmpt  46233  limsupresuz  46277  liminfresuz  46358  coskpi2  46440  cosknegpi  46443  dvsinax  46487  dvnmptdivc  46512  dvnxpaek  46516  dvnmul  46517  dvmptfprodlem  46518  ditgeqiooicc  46534  itgioocnicc  46551  itgspltprt  46553  wallispi2lem2  46646  dirkerper  46670  dirkertrigeqlem2  46673  dirkertrigeqlem3  46674  dirkertrigeq  46675  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem18  46699  fourierdlem19  46700  fourierdlem33  46714  fourierdlem35  46716  fourierdlem41  46722  fourierdlem42  46723  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem53  46733  fourierdlem63  46743  fourierdlem65  46745  fourierdlem73  46753  fourierdlem74  46754  fourierdlem75  46755  fourierdlem81  46761  fourierdlem82  46762  fourierdlem83  46763  fourierdlem84  46764  fourierdlem90  46770  fourierdlem93  46773  fourierdlem95  46775  fourierdlem103  46783  fourierdlem104  46784  fourierdlem107  46787  fourierdlem111  46791  fourierswlem  46804  fouriersw  46805  etransclem4  46812  etransclem9  46817  etransclem28  46836  etransclem35  46843  etransclem38  46846  sge0tsms  46954  sge0sup  46965  sge0resplit  46980  sge0split  46983  sge0ss  46986  sge0rpcpnf  46995  sge0isum  47001  sge0xadd  47009  sge0seq  47020  ismeannd  47041  caratheodorylem1  47100  isomenndlem  47104  hoicvrrex  47130  ovn0lem  47139  hoidmvlelem2  47170  hoidmvlelem3  47171  ovnlecvr2  47184  voncmpl  47195  hspmbllem1  47200  hspmbllem2  47201  ovolval4lem1  47223  incsmf  47316  smfpimltmpt  47320  smfpimltxrmptf  47332  decsmf  47341  smfpimgtmpt  47355  smfpimgtxrmptf  47358  smfmullem1  47365  smflimsuplem2  47395  sigarac  47426  cevathlem2  47442  sin3t  47465  cos3t  47466  m1modmmod  47958  fmtnorec3  48157  fmtnorec4  48158  oddflALTV  48285  perfectALTVlem2  48344  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  uspgrlimlem1  48610  gpgvtxedg0  48685  gpgvtxedg1  48686  gpg3kgrtriexlem2  48706  ply1mulgsum  49012  lindslinindsimp2lem5  49084  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdiglem2  49244  itschlc0yqe  49382