Theorem 3eqtrrd 2661

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	|- ( ph -> A = B )
3eqtrd.2	|- ( ph -> B = C )
3eqtrd.3	|- ( ph -> C = D )

Assertion

Ref	Expression
3eqtrrd	|- ( ph -> D = A )

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. . 3 |- ( ph -> A = B )
2		3eqtrd.2	. . 3 |- ( ph -> B = C )
3	1, 2	eqtrd 2656	. 2 |- ( ph -> A = C )
4		3eqtrd.3	. 2 |- ( ph -> C = D )
5	3, 4	eqtr2d 2657	1 |- ( ph -> D = A )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  fimacnvinrn  6348  fvcofneq  6367  iunfictbso  8937  axcnre  9985  fseq1p1m1  12414  seqf1olem1  12840  expmulz  12906  expubnd  12921  subsq  12972  bcm1k  13102  bcpasc  13108  cshwcshid  13573  crim  13855  rereb  13860  rlimrecl  14311  iseraltlem2  14413  fsumparts  14538  isumshft  14571  geoserg  14598  efsub  14830  sincossq  14906  efieq1re  14929  eucalg  15300  lcmfunsnlem  15354  phiprmpw  15481  modprmn0modprm0  15512  coprimeprodsq  15513  pythagtriplem15  15534  pythagtriplem17  15536  fldivp1  15601  1arithlem4  15630  setsidvald  15889  setsid  15914  pwsbas  16147  invfuc  16634  latdisdlem  17189  odinv  17978  frgpuplem  18185  gexexlem  18255  srgbinomlem4  18543  gsumdixp  18609  mplcoe1  19465  evlsvarsrng  19528  ply1idvr1  19663  ply1coe  19666  evls1varsrng  19704  cnfldsub  19774  mat1scmat  20345  m1detdiag  20403  mdetunilem7  20424  madugsum  20449  pm2mpmhmlem2  20624  mretopd  20896  upxp  21426  uptx  21428  imasdsf1olem  22178  clmvs2  22894  cphipipcj  23000  cphipval2  23040  itgmulc2lem2  23599  r1pid  23919  coeeulem  23980  fta1lem  24062  aaliou3lem8  24100  eff1olem  24294  tanarg  24365  logcnlem4  24391  root1cj  24497  angpieqvdlem  24555  quad2  24566  dcubic  24573  quart1  24583  jensen  24715  lgamgulmlem5  24759  lgamgulm2  24762  ftalem5  24803  basellem8  24814  chpchtsum  24944  logfaclbnd  24947  perfectlem2  24955  gausslemma2dlem1a  25090  2sqlem3  25145  dchrvmasum2lem  25185  dchrvmasumiflem2  25191  selberglem2  25235  selberg3r  25258  pntlem3  25298  ostth2  25326  ostth3  25327  krippenlem  25585  colinearalglem1  25786  axlowdimlem16  25837  axcontlem4  25847  nmbdoplbi  28883  nmcopexi  28886  nmbdfnlbi  28908  nmcfnexi  28910  nmcfnlbi  28911  hstoh  29091  fcobij  29500  lt2addrd  29516  xlt2addrd  29523  isarchi3  29741  archirngz  29743  symgfcoeu  29845  submatminr1  29876  mdetpmtr1  29889  madjusmdetlem1  29893  qqhnm  30034  esumfzf  30131  ddemeas  30299  sseqp1  30457  ballotlemi1  30564  ballotlemii  30565  ballotlemic  30568  ballotlem1c  30569  fsum2dsub  30685  circlemeth  30718  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  elmrsubrn  31417  cos2h  33400  itg2addnclem  33461  itgmulc2nclem2  33477  areacirclem1  33500  areacirclem4  33503  cntotbnd  33595  atmod2i2  35148  trljat1  35453  trljat2  35454  cdleme9  35540  cdleme15b  35562  cdleme20c  35599  cdleme22eALTN  35633  dvhopN  36405  doca2N  36415  cdlemn10  36495  dochocss  36655  djhlj  36690  dihprrnlem1N  36713  dihprrnlem2  36714  lcfl7lem  36788  lclkrlem2c  36798  hgmapadd  37186  hdmapinvlem3  37212  hgmapvvlem1  37215  rmydbl  37505  jm2.18  37555  jm2.19  37560  proot1hash  37778  dssmapnvod  38314  binomcxplemnotnn0  38555  oddfl  39489  dstregt0  39493  supsubc  39569  absimlere  39710  uzinico2  39789  fsumsplit1  39804  mccllem  39829  ellimcabssub0  39849  sumnnodd  39862  climresmpt  39891  limsupresuz  39935  liminfresuz  40016  coskpi2  40077  cosknegpi  40080  dvsinax  40127  dvnmptdivc  40153  dvnxpaek  40157  dvnmul  40158  dvmptfprodlem  40159  ditgeqiooicc  40176  itgioocnicc  40193  itgspltprt  40195  wallispi2lem2  40289  dirkerper  40313  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem18  40342  fourierdlem19  40343  fourierdlem33  40357  fourierdlem35  40359  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem53  40376  fourierdlem63  40386  fourierdlem65  40388  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem90  40413  fourierdlem93  40416  fourierdlem95  40418  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem111  40434  fourierswlem  40447  fouriersw  40448  etransclem4  40455  etransclem9  40460  etransclem28  40479  etransclem35  40486  etransclem38  40489  sge0tsms  40597  sge0sup  40608  sge0resplit  40623  sge0split  40626  sge0ss  40629  sge0rpcpnf  40638  sge0isum  40644  sge0xadd  40652  sge0seq  40663  ismeannd  40684  caratheodorylem1  40740  isomenndlem  40744  hoicvrrex  40770  ovn0lem  40779  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnlecvr2  40824  voncmpl  40835  hspmbllem1  40840  hspmbllem2  40841  ovolval4lem1  40863  incsmf  40951  smfpimltmpt  40955  smfpimltxrmpt  40967  decsmf  40975  smfpimgtmpt  40989  smfpimgtxrmpt  40992  smfmullem1  40998  smfsupmpt  41021  smfinfmpt  41025  smflimsuplem2  41027  sigarac  41041  cevathlem2  41057  fmtnorec3  41460  fmtnorec4  41461  pwdif  41501  oddflALTV  41575  perfectALTVlem2  41631  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  c0snmgmhm  41914  funcrngcsetc  41998  funcringcsetc  42035  ply1mulgsum  42178  lindslinindsimp2lem5  42251  m1modmmod  42316  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem2  42416