Theorem 3eqtrrd 2801

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 2796	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2797	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 2155  ax-ext 2733

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

This theorem is used by:  fimacnvinrn  7071  fvcofneq  7093  iunfictbso  10193  axcnre  11249  fseq1p1m1  13732  seqf1olem1  14184  expmulz  14251  expubnd  14321  subsq  14354  bcm1k  14459  bcpasc  14465  cshwcshid  14978  crim  15282  rereb  15287  rlimrecl  15747  iseraltlem2  15850  fsumsplit1  15911  fsumparts  15973  isumshft  16008  geoserg  16035  pwdif  16037  efsub  16268  sincossq  16344  efieq1re  16367  nn0expgcd  16738  eucalg  16762  lcmfunsnlem  16816  phiprmpw  16953  modprmn0modprm0  16985  coprimeprodsq  16986  pythagtriplem15  17007  pythagtriplem17  17009  fldivp1  17075  1arithlem4  17104  setsidvald  17377  setsid  17385  pwsbas  17658  invfuc  18152  estrreslem1  18311  latdisdlem  18670  ghmquskerco  19498  odinv  19775  frgpuplem  19986  gexexlem  20066  fincygsubgodd  20328  srgbinomlem4  20455  gsumdixp  20548  c0snmgmhm  20692  funcrngcsetc  20892  funcringcsetc  20926  cnfldsub  21706  mplcoe1  22346  evlsvarsrng  22416  selvvvval  22451  psdmul  22487  ply1coe  22616  evls1varsrng  22658  mat1scmat  22854  m1detdiag  22912  mdetunilem7  22933  madugsum  22958  pm2mpmhmlem2  23137  mretopd  23410  upxp  23942  uptx  23944  imasdsf1olem  24692  clmvs2  25415  cphipipcj  25521  cphipval2  25562  itgmulc2lem2  26153  r1pid  26479  coeeulem  26543  fta1lem  26628  aaliou3lem8  26672  eff1olem  26876  tanarg  26947  logcnlem4  26973  root1cj  27084  angpieqvdlem  27156  quad2  27167  dcubic  27174  quart1  27184  jensen  27316  lgamgulmlem5  27360  lgamgulm2  27363  ftalem5  27404  basellem8  27415  chpchtsum  27546  logfaclbnd  27549  perfectlem2  27557  gausslemma2dlem1a  27692  2sqlem3  27747  dchrvmasum2lem  27823  dchrvmasumiflem2  27829  selberglem2  27873  selberg3r  27896  pntlem3  27936  ostth2  27964  ostth3  27965  madeoldsuc  28271  zseo  28808  addhalfcut  28845  pw2cut2  28848  krippenlem  29162  colinearalglem1  29484  axlowdimlem16  29535  axcontlem4  29545  clwlkclwwlkfo  30600  nmbdoplbi  32626  nmcopexi  32629  nmbdfnlbi  32651  nmcfnexi  32653  nmcfnlbi  32654  hstoh  32834  fcobij  33312  lt2addrd  33342  xlt2addrd  33351  cshwrnid  33522  symgfcoeu  33643  cycpmconjslem2  33716  cycpmconjs  33717  isarchi3  33748  archirngz  33750  elrgspnsubrunlem1  33808  elrspunsn  33979  mxidlirredi  33996  1arithidomlem1  34067  1arithidomlem2  34068  1arithidom  34069  evlextv  34174  esplyfval1  34205  dimkerim  34259  lvecendof1f1o  34265  fldextrspunlsplem  34305  nn0constr  34393  constraddcl  34394  constrnegcl  34395  constrremulcl  34399  constrrecl  34401  constrimcl  34402  constrmulcl  34403  constrreinvcl  34404  constrinvcl  34405  constrresqrtcl  34409  constrabscl  34410  2sqr3minply  34412  submatminr1  34442  mdetpmtr1  34455  madjusmdetlem1  34459  zarcmplem  34513  qqhnm  34622  esumfzf  34701  ddemeas  34869  sseqp1  35027  ballotlemi1  35135  ballotlemii  35136  ballotlemic  35139  ballotlem1c  35140  fsum2dsub  35236  circlemeth  35269  hgt750lemb  35285  hgt750lema  35286  hgt750leme  35287  elmrsubrn  36285  nadddilem1  36969  cos2h  38534  itg2addnclem  38589  itgmulc2nclem2  38605  areacirclem1  38626  areacirclem4  38629  cntotbnd  38730  atmod2i2  40919  trljat1  41223  trljat2  41224  cdleme9  41310  cdleme15b  41332  cdleme20c  41368  cdleme22eALTN  41402  dvhopN  42173  doca2N  42183  cdlemn10  42263  dochocss  42423  djhlj  42458  dihprrnlem1N  42481  dihprrnlem2  42482  lcfl7lem  42556  lclkrlem2c  42566  hgmapadd  42951  hdmapinvlem3  42977  hgmapvvlem1  42980  sumcubes  43370  zaddcomlem  43527  fidomncyc  43599  rmydbl  43946  jm2.18  43994  jm2.19  43999  proot1hash  44196  dssmapnvod  45019  binomcxplemnotnn0  45339  oddfl  46293  dstregt0  46297  supsubc  46364  absimlere  46488  uzinico2  46572  mccllem  46608  ellimcabssub0  46628  sumnnodd  46641  climresmpt  46668  limsupresuz  46712  liminfresuz  46793  coskpi2  46875  cosknegpi  46878  dvsinax  46922  dvnmptdivc  46947  dvnxpaek  46951  dvnmul  46952  dvmptfprodlem  46953  ditgeqiooicc  46969  itgioocnicc  46986  itgspltprt  46988  wallispi2lem2  47081  dirkerper  47105  dirkertrigeqlem2  47108  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem18  47134  fourierdlem19  47135  fourierdlem33  47149  fourierdlem35  47151  fourierdlem41  47157  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem53  47168  fourierdlem63  47178  fourierdlem65  47180  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem81  47196  fourierdlem82  47197  fourierdlem83  47198  fourierdlem84  47199  fourierdlem90  47205  fourierdlem93  47208  fourierdlem95  47210  fourierdlem103  47218  fourierdlem104  47219  fourierdlem107  47222  fourierdlem111  47226  fourierswlem  47239  fouriersw  47240  etransclem4  47247  etransclem9  47252  etransclem28  47271  etransclem35  47278  etransclem38  47281  sge0tsms  47389  sge0sup  47400  sge0resplit  47415  sge0split  47418  sge0ss  47421  sge0rpcpnf  47430  sge0isum  47436  sge0xadd  47444  sge0seq  47455  ismeannd  47476  caratheodorylem1  47535  isomenndlem  47539  hoicvrrex  47565  ovn0lem  47574  hoidmvlelem2  47605  hoidmvlelem3  47606  ovnlecvr2  47619  voncmpl  47630  hspmbllem1  47635  hspmbllem2  47636  ovolval4lem1  47658  incsmf  47751  smfpimltmpt  47755  smfpimltxrmptf  47767  decsmf  47776  smfpimgtmpt  47790  smfpimgtxrmptf  47793  smfmullem1  47800  smflimsuplem2  47830  sigarac  47861  cevathlem2  47877  sin3t  47916  cos3t  47917  m1modmmod  48433  fmtnorec3  48632  fmtnorec4  48633  oddflALTV  48760  perfectALTVlem2  48819  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  uspgrlimlem1  49085  gpgvtxedg0  49160  gpgvtxedg1  49161  gpg3kgrtriexlem2  49181  ply1mulgsum  49501  lindslinindsimp2lem5  49573  nn0sumshdiglemA  49730  nn0sumshdiglemB  49731  nn0sumshdiglem2  49733  itschlc0yqe  49871