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  6834  fvcofneq  6853  iunfictbso  9534  axcnre  10580  fseq1p1m1  12975  seqf1olem1  13403  expmulz  13469  expubnd  13535  subsq  13566  bcm1k  13669  bcpasc  13675  cshwcshid  14183  crim  14468  rereb  14473  rlimrecl  14931  iseraltlem2  15033  fsumparts  15155  isumshft  15188  geoserg  15215  pwdif  15217  efsub  15447  sincossq  15523  efieq1re  15546  eucalg  15925  lcmfunsnlem  15979  phiprmpw  16107  modprmn0modprm0  16138  coprimeprodsq  16139  pythagtriplem15  16160  pythagtriplem17  16162  fldivp1  16227  1arithlem4  16256  setsidvald  16508  setsid  16532  pwsbas  16754  invfuc  17238  latdisdlem  17793  odinv  18682  frgpuplem  18892  gexexlem  18966  fincygsubgodd  19228  srgbinomlem4  19287  gsumdixp  19353  mplcoe1  20240  evlsvarsrng  20306  ply1idvr1  20455  ply1coe  20458  evls1varsrng  20497  cnfldsub  20567  mat1scmat  21142  m1detdiag  21200  mdetunilem7  21221  madugsum  21246  pm2mpmhmlem2  21421  mretopd  21694  upxp  22225  uptx  22227  imasdsf1olem  22977  clmvs2  23692  cphipipcj  23798  cphipval2  23838  itgmulc2lem2  24427  r1pid  24747  coeeulem  24808  fta1lem  24890  aaliou3lem8  24928  eff1olem  25126  tanarg  25196  logcnlem4  25222  root1cj  25331  angpieqvdlem  25400  quad2  25411  dcubic  25418  quart1  25428  jensen  25560  lgamgulmlem5  25604  lgamgulm2  25607  ftalem5  25648  basellem8  25659  chpchtsum  25789  logfaclbnd  25792  perfectlem2  25800  gausslemma2dlem1a  25935  2sqlem3  25990  dchrvmasum2lem  26066  dchrvmasumiflem2  26072  selberglem2  26116  selberg3r  26139  pntlem3  26179  ostth2  26207  ostth3  26208  krippenlem  26470  colinearalglem1  26686  axlowdimlem16  26737  axcontlem4  26747  clwlkclwwlkfo  27781  nmbdoplbi  29795  nmcopexi  29798  nmbdfnlbi  29820  nmcfnexi  29822  nmcfnlbi  29823  hstoh  30003  fcobij  30452  lt2addrd  30469  xlt2addrd  30476  cshwrnid  30630  symgfcoeu  30721  cycpmconjslem2  30792  cycpmconjs  30793  isarchi3  30811  archirngz  30813  dimkerim  31018  submatminr1  31070  mdetpmtr1  31083  madjusmdetlem1  31087  qqhnm  31226  esumfzf  31323  ddemeas  31490  sseqp1  31648  ballotlemi1  31755  ballotlemii  31756  ballotlemic  31759  ballotlem1c  31760  fsum2dsub  31873  circlemeth  31906  hgt750lemb  31922  hgt750lema  31923  hgt750leme  31924  elmrsubrn  32762  cos2h  34877  itg2addnclem  34937  itgmulc2nclem2  34953  areacirclem1  34976  areacirclem4  34979  cntotbnd  35068  atmod2i2  36992  trljat1  37296  trljat2  37297  cdleme9  37383  cdleme15b  37405  cdleme20c  37441  cdleme22eALTN  37475  dvhopN  38246  doca2N  38256  cdlemn10  38336  dochocss  38496  djhlj  38531  dihprrnlem1N  38554  dihprrnlem2  38555  lcfl7lem  38629  lclkrlem2c  38639  hgmapadd  39024  hdmapinvlem3  39050  hgmapvvlem1  39053  nn0expgcd  39177  rmydbl  39530  jm2.18  39578  jm2.19  39583  proot1hash  39793  dssmapnvod  40359  binomcxplemnotnn0  40681  oddfl  41536  dstregt0  41540  supsubc  41614  absimlere  41749  uzinico2  41831  fsumsplit1  41846  mccllem  41871  ellimcabssub0  41891  sumnnodd  41904  climresmpt  41933  limsupresuz  41977  liminfresuz  42058  coskpi2  42140  cosknegpi  42143  dvsinax  42190  dvnmptdivc  42216  dvnxpaek  42220  dvnmul  42221  dvmptfprodlem  42222  ditgeqiooicc  42238  itgioocnicc  42255  itgspltprt  42257  wallispi2lem2  42351  dirkerper  42375  dirkertrigeqlem2  42378  dirkertrigeqlem3  42379  dirkertrigeq  42380  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem18  42404  fourierdlem19  42405  fourierdlem33  42419  fourierdlem35  42421  fourierdlem41  42427  fourierdlem42  42428  fourierdlem48  42433  fourierdlem49  42434  fourierdlem50  42435  fourierdlem53  42438  fourierdlem63  42448  fourierdlem65  42450  fourierdlem73  42458  fourierdlem74  42459  fourierdlem75  42460  fourierdlem81  42466  fourierdlem82  42467  fourierdlem83  42468  fourierdlem84  42469  fourierdlem90  42475  fourierdlem93  42478  fourierdlem95  42480  fourierdlem103  42488  fourierdlem104  42489  fourierdlem107  42492  fourierdlem111  42496  fourierswlem  42509  fouriersw  42510  etransclem4  42517  etransclem9  42522  etransclem28  42541  etransclem35  42548  etransclem38  42551  sge0tsms  42656  sge0sup  42667  sge0resplit  42682  sge0split  42685  sge0ss  42688  sge0rpcpnf  42697  sge0isum  42703  sge0xadd  42711  sge0seq  42722  ismeannd  42743  caratheodorylem1  42802  isomenndlem  42806  hoicvrrex  42832  ovn0lem  42841  hoidmvlelem2  42872  hoidmvlelem3  42873  ovnlecvr2  42886  voncmpl  42897  hspmbllem1  42902  hspmbllem2  42903  ovolval4lem1  42925  incsmf  43013  smfpimltmpt  43017  smfpimltxrmpt  43029  decsmf  43037  smfpimgtmpt  43051  smfpimgtxrmpt  43054  smfmullem1  43060  smfsupmpt  43083  smfinfmpt  43087  smflimsuplem2  43089  sigarac  43103  cevathlem2  43119  fmtnorec3  43704  fmtnorec4  43705  oddflALTV  43822  perfectALTVlem2  43881  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  c0snmgmhm  44179  funcrngcsetc  44263  funcringcsetc  44300  ply1mulgsum  44438  lindslinindsimp2lem5  44511  m1modmmod  44575  nn0sumshdiglemA  44673  nn0sumshdiglemB  44674  nn0sumshdiglem2  44676  itschlc0yqe  44741