Theorem 3eqtrrd 2861

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  fimacnvinrn  6839  fvcofneq  6858  iunfictbso  9539  axcnre  10585  fseq1p1m1  12980  seqf1olem1  13408  expmulz  13474  expubnd  13540  subsq  13571  bcm1k  13674  bcpasc  13680  cshwcshid  14188  crim  14473  rereb  14478  rlimrecl  14936  iseraltlem2  15038  fsumparts  15160  isumshft  15193  geoserg  15220  pwdif  15222  efsub  15452  sincossq  15528  efieq1re  15551  eucalg  15930  lcmfunsnlem  15984  phiprmpw  16112  modprmn0modprm0  16143  coprimeprodsq  16144  pythagtriplem15  16165  pythagtriplem17  16167  fldivp1  16232  1arithlem4  16261  setsidvald  16513  setsid  16537  pwsbas  16759  invfuc  17243  latdisdlem  17798  odinv  18687  frgpuplem  18897  gexexlem  18971  fincygsubgodd  19233  srgbinomlem4  19292  gsumdixp  19358  mplcoe1  20245  evlsvarsrng  20311  ply1idvr1  20460  ply1coe  20463  evls1varsrng  20502  cnfldsub  20572  mat1scmat  21147  m1detdiag  21205  mdetunilem7  21226  madugsum  21251  pm2mpmhmlem2  21426  mretopd  21699  upxp  22230  uptx  22232  imasdsf1olem  22982  clmvs2  23697  cphipipcj  23803  cphipval2  23843  itgmulc2lem2  24432  r1pid  24752  coeeulem  24813  fta1lem  24895  aaliou3lem8  24933  eff1olem  25131  tanarg  25201  logcnlem4  25227  root1cj  25336  angpieqvdlem  25405  quad2  25416  dcubic  25423  quart1  25433  jensen  25565  lgamgulmlem5  25609  lgamgulm2  25612  ftalem5  25653  basellem8  25664  chpchtsum  25794  logfaclbnd  25797  perfectlem2  25805  gausslemma2dlem1a  25940  2sqlem3  25995  dchrvmasum2lem  26071  dchrvmasumiflem2  26077  selberglem2  26121  selberg3r  26144  pntlem3  26184  ostth2  26212  ostth3  26213  krippenlem  26475  colinearalglem1  26691  axlowdimlem16  26742  axcontlem4  26752  clwlkclwwlkfo  27786  nmbdoplbi  29800  nmcopexi  29803  nmbdfnlbi  29825  nmcfnexi  29827  nmcfnlbi  29828  hstoh  30008  fcobij  30457  lt2addrd  30474  xlt2addrd  30481  cshwrnid  30635  symgfcoeu  30726  cycpmconjslem2  30797  cycpmconjs  30798  isarchi3  30816  archirngz  30818  dimkerim  31023  submatminr1  31075  mdetpmtr1  31088  madjusmdetlem1  31092  qqhnm  31231  esumfzf  31328  ddemeas  31495  sseqp1  31653  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  fsum2dsub  31878  circlemeth  31911  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  elmrsubrn  32767  cos2h  34882  itg2addnclem  34942  itgmulc2nclem2  34958  areacirclem1  34981  areacirclem4  34984  cntotbnd  35073  atmod2i2  36997  trljat1  37301  trljat2  37302  cdleme9  37388  cdleme15b  37410  cdleme20c  37446  cdleme22eALTN  37480  dvhopN  38251  doca2N  38261  cdlemn10  38341  dochocss  38501  djhlj  38536  dihprrnlem1N  38559  dihprrnlem2  38560  lcfl7lem  38634  lclkrlem2c  38644  hgmapadd  39029  hdmapinvlem3  39055  hgmapvvlem1  39058  nn0expgcd  39182  rmydbl  39535  jm2.18  39583  jm2.19  39588  proot1hash  39798  dssmapnvod  40364  binomcxplemnotnn0  40686  oddfl  41541  dstregt0  41545  supsubc  41619  absimlere  41754  uzinico2  41836  fsumsplit1  41851  mccllem  41876  ellimcabssub0  41896  sumnnodd  41909  climresmpt  41938  limsupresuz  41982  liminfresuz  42063  coskpi2  42145  cosknegpi  42148  dvsinax  42195  dvnmptdivc  42221  dvnxpaek  42225  dvnmul  42226  dvmptfprodlem  42227  ditgeqiooicc  42243  itgioocnicc  42260  itgspltprt  42262  wallispi2lem2  42356  dirkerper  42380  dirkertrigeqlem2  42383  dirkertrigeqlem3  42384  dirkertrigeq  42385  dirkercncflem2  42388  dirkercncflem4  42390  fourierdlem18  42409  fourierdlem19  42410  fourierdlem33  42424  fourierdlem35  42426  fourierdlem41  42432  fourierdlem42  42433  fourierdlem48  42438  fourierdlem49  42439  fourierdlem50  42440  fourierdlem53  42443  fourierdlem63  42453  fourierdlem65  42455  fourierdlem73  42463  fourierdlem74  42464  fourierdlem75  42465  fourierdlem81  42471  fourierdlem82  42472  fourierdlem83  42473  fourierdlem84  42474  fourierdlem90  42480  fourierdlem93  42483  fourierdlem95  42485  fourierdlem103  42493  fourierdlem104  42494  fourierdlem107  42497  fourierdlem111  42501  fourierswlem  42514  fouriersw  42515  etransclem4  42522  etransclem9  42527  etransclem28  42546  etransclem35  42553  etransclem38  42556  sge0tsms  42661  sge0sup  42672  sge0resplit  42687  sge0split  42690  sge0ss  42693  sge0rpcpnf  42702  sge0isum  42708  sge0xadd  42716  sge0seq  42727  ismeannd  42748  caratheodorylem1  42807  isomenndlem  42811  hoicvrrex  42837  ovn0lem  42846  hoidmvlelem2  42877  hoidmvlelem3  42878  ovnlecvr2  42891  voncmpl  42902  hspmbllem1  42907  hspmbllem2  42908  ovolval4lem1  42930  incsmf  43018  smfpimltmpt  43022  smfpimltxrmpt  43034  decsmf  43042  smfpimgtmpt  43056  smfpimgtxrmpt  43059  smfmullem1  43065  smfsupmpt  43088  smfinfmpt  43092  smflimsuplem2  43094  sigarac  43108  cevathlem2  43124  fmtnorec3  43709  fmtnorec4  43710  oddflALTV  43827  perfectALTVlem2  43886  nnsum4primeseven  43964  nnsum4primesevenALTV  43965  c0snmgmhm  44184  funcrngcsetc  44268  funcringcsetc  44305  ply1mulgsum  44443  lindslinindsimp2lem5  44516  m1modmmod  44580  nn0sumshdiglemA  44678  nn0sumshdiglemB  44679  nn0sumshdiglem2  44681  itschlc0yqe  44746