Theorem 3eqtrrd 2781

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728

This theorem is referenced by:  fimacnvinrn  7022  fvcofneq  7042  iunfictbso  10049  axcnre  11099  fseq1p1m1  13514  seqf1olem1  13946  expmulz  14013  expubnd  14081  subsq  14113  bcm1k  14214  bcpasc  14220  cshwcshid  14715  crim  14999  rereb  15004  rlimrecl  15461  iseraltlem2  15566  fsumsplit1  15629  fsumparts  15690  isumshft  15723  geoserg  15750  pwdif  15752  efsub  15981  sincossq  16057  efieq1re  16080  eucalg  16462  lcmfunsnlem  16516  phiprmpw  16647  modprmn0modprm0  16678  coprimeprodsq  16679  pythagtriplem15  16700  pythagtriplem17  16702  fldivp1  16768  1arithlem4  16797  setsidvald  17070  setsidvaldOLD  17071  setsid  17079  pwsbas  17368  invfuc  17862  estrreslem1  18023  latdisdlem  18384  odinv  19341  frgpuplem  19552  gexexlem  19628  fincygsubgodd  19889  srgbinomlem4  19958  gsumdixp  20031  cnfldsub  20823  mplcoe1  21436  evlsvarsrng  21507  ply1idvr1  21662  ply1coe  21665  evls1varsrng  21704  mat1scmat  21886  m1detdiag  21944  mdetunilem7  21965  madugsum  21990  pm2mpmhmlem2  22166  mretopd  22441  upxp  22972  uptx  22974  imasdsf1olem  23724  clmvs2  24455  cphipipcj  24562  cphipval2  24603  itgmulc2lem2  25195  r1pid  25522  coeeulem  25583  fta1lem  25665  aaliou3lem8  25703  eff1olem  25902  tanarg  25972  logcnlem4  25998  root1cj  26107  angpieqvdlem  26176  quad2  26187  dcubic  26194  quart1  26204  jensen  26336  lgamgulmlem5  26380  lgamgulm2  26383  ftalem5  26424  basellem8  26435  chpchtsum  26565  logfaclbnd  26568  perfectlem2  26576  gausslemma2dlem1a  26711  2sqlem3  26766  dchrvmasum2lem  26842  dchrvmasumiflem2  26848  selberglem2  26892  selberg3r  26915  pntlem3  26955  ostth2  26983  ostth3  26984  madeoldsuc  27212  krippenlem  27630  colinearalglem1  27853  axlowdimlem16  27904  axcontlem4  27914  clwlkclwwlkfo  28951  nmbdoplbi  30964  nmcopexi  30967  nmbdfnlbi  30989  nmcfnexi  30991  nmcfnlbi  30992  hstoh  31172  fcobij  31634  lt2addrd  31651  xlt2addrd  31658  cshwrnid  31810  symgfcoeu  31928  cycpmconjslem2  31999  cycpmconjs  32000  isarchi3  32018  archirngz  32020  dimkerim  32313  submatminr1  32382  mdetpmtr1  32395  madjusmdetlem1  32399  zarcmplem  32453  qqhnm  32562  esumfzf  32659  ddemeas  32826  sseqp1  32986  ballotlemi1  33093  ballotlemii  33094  ballotlemic  33097  ballotlem1c  33098  fsum2dsub  33211  circlemeth  33244  hgt750lemb  33260  hgt750lema  33261  hgt750leme  33262  elmrsubrn  34105  cos2h  36060  itg2addnclem  36120  itgmulc2nclem2  36136  areacirclem1  36157  areacirclem4  36160  cntotbnd  36246  atmod2i2  38316  trljat1  38620  trljat2  38621  cdleme9  38707  cdleme15b  38729  cdleme20c  38765  cdleme22eALTN  38799  dvhopN  39570  doca2N  39580  cdlemn10  39660  dochocss  39820  djhlj  39855  dihprrnlem1N  39878  dihprrnlem2  39879  lcfl7lem  39953  lclkrlem2c  39963  hgmapadd  40348  hdmapinvlem3  40374  hgmapvvlem1  40377  nn0expgcd  40799  zaddcomlem  40898  rmydbl  41242  jm2.18  41290  jm2.19  41295  proot1hash  41505  dssmapnvod  42274  binomcxplemnotnn0  42618  oddfl  43487  dstregt0  43491  supsubc  43563  absimlere  43691  uzinico2  43772  mccllem  43810  ellimcabssub0  43830  sumnnodd  43843  climresmpt  43872  limsupresuz  43916  liminfresuz  43997  coskpi2  44079  cosknegpi  44082  dvsinax  44126  dvnmptdivc  44151  dvnxpaek  44155  dvnmul  44156  dvmptfprodlem  44157  ditgeqiooicc  44173  itgioocnicc  44190  itgspltprt  44192  wallispi2lem2  44285  dirkerper  44309  dirkertrigeqlem2  44312  dirkertrigeqlem3  44313  dirkertrigeq  44314  dirkercncflem2  44317  dirkercncflem4  44319  fourierdlem18  44338  fourierdlem19  44339  fourierdlem33  44353  fourierdlem35  44355  fourierdlem41  44361  fourierdlem42  44362  fourierdlem48  44367  fourierdlem49  44368  fourierdlem50  44369  fourierdlem53  44372  fourierdlem63  44382  fourierdlem65  44384  fourierdlem73  44392  fourierdlem74  44393  fourierdlem75  44394  fourierdlem81  44400  fourierdlem82  44401  fourierdlem83  44402  fourierdlem84  44403  fourierdlem90  44409  fourierdlem93  44412  fourierdlem95  44414  fourierdlem103  44422  fourierdlem104  44423  fourierdlem107  44426  fourierdlem111  44430  fourierswlem  44443  fouriersw  44444  etransclem4  44451  etransclem9  44456  etransclem28  44475  etransclem35  44482  etransclem38  44485  sge0tsms  44593  sge0sup  44604  sge0resplit  44619  sge0split  44622  sge0ss  44625  sge0rpcpnf  44634  sge0isum  44640  sge0xadd  44648  sge0seq  44659  ismeannd  44680  caratheodorylem1  44739  isomenndlem  44743  hoicvrrex  44769  ovn0lem  44778  hoidmvlelem2  44809  hoidmvlelem3  44810  ovnlecvr2  44823  voncmpl  44834  hspmbllem1  44839  hspmbllem2  44840  ovolval4lem1  44862  incsmf  44955  smfpimltmpt  44959  smfpimltxrmptf  44971  decsmf  44980  smfpimgtmpt  44994  smfpimgtxrmptf  44997  smfmullem1  45004  smfinfmpt  45032  smflimsuplem2  45034  sigarac  45065  cevathlem2  45081  fmtnorec3  45712  fmtnorec4  45713  oddflALTV  45827  perfectALTVlem2  45886  nnsum4primeseven  45964  nnsum4primesevenALTV  45965  c0snmgmhm  46184  funcrngcsetc  46268  funcringcsetc  46305  ply1mulgsum  46443  lindslinindsimp2lem5  46515  m1modmmod  46579  nn0sumshdiglemA  46677  nn0sumshdiglemB  46678  nn0sumshdiglem2  46680  itschlc0yqe  46818