Theorem 3eqtrrd 2769

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  fimacnvinrn  7005  fvcofneq  7027  iunfictbso  10008  axcnre  11058  fseq1p1m1  13501  seqf1olem1  13948  expmulz  14015  expubnd  14085  subsq  14117  bcm1k  14222  bcpasc  14228  cshwcshid  14734  crim  15022  rereb  15027  rlimrecl  15487  iseraltlem2  15590  fsumsplit1  15652  fsumparts  15713  isumshft  15746  geoserg  15773  pwdif  15775  efsub  16009  sincossq  16085  efieq1re  16108  nn0expgcd  16475  eucalg  16498  lcmfunsnlem  16552  phiprmpw  16687  modprmn0modprm0  16719  coprimeprodsq  16720  pythagtriplem15  16741  pythagtriplem17  16743  fldivp1  16809  1arithlem4  16838  setsidvald  17110  setsid  17118  pwsbas  17391  invfuc  17884  estrreslem1  18043  latdisdlem  18402  ghmquskerco  19163  odinv  19440  frgpuplem  19651  gexexlem  19731  fincygsubgodd  19993  srgbinomlem4  20114  gsumdixp  20204  c0snmgmhm  20347  funcrngcsetc  20525  funcringcsetc  20559  cnfldsub  21304  mplcoe1  21942  evlsvarsrng  22004  psdmul  22051  ply1idvr1OLD  22180  ply1coe  22183  evls1varsrng  22225  mat1scmat  22424  m1detdiag  22482  mdetunilem7  22503  madugsum  22528  pm2mpmhmlem2  22704  mretopd  22977  upxp  23508  uptx  23510  imasdsf1olem  24259  clmvs2  24992  cphipipcj  25098  cphipval2  25139  itgmulc2lem2  25732  r1pid  26064  coeeulem  26127  fta1lem  26213  aaliou3lem8  26251  eff1olem  26455  tanarg  26526  logcnlem4  26552  root1cj  26664  angpieqvdlem  26736  quad2  26747  dcubic  26754  quart1  26764  jensen  26897  lgamgulmlem5  26941  lgamgulm2  26944  ftalem5  26985  basellem8  26996  chpchtsum  27128  logfaclbnd  27131  perfectlem2  27139  gausslemma2dlem1a  27274  2sqlem3  27329  dchrvmasum2lem  27405  dchrvmasumiflem2  27411  selberglem2  27455  selberg3r  27478  pntlem3  27518  ostth2  27546  ostth3  27547  madeoldsuc  27799  zseo  28314  addhalfcut  28347  krippenlem  28635  colinearalglem1  28851  axlowdimlem16  28902  axcontlem4  28912  clwlkclwwlkfo  29953  nmbdoplbi  31968  nmcopexi  31971  nmbdfnlbi  31993  nmcfnexi  31995  nmcfnlbi  31996  hstoh  32176  fcobij  32665  lt2addrd  32695  xlt2addrd  32703  cshwrnid  32904  symgfcoeu  33025  cycpmconjslem2  33098  cycpmconjs  33099  isarchi3  33130  archirngz  33132  elrgspnsubrunlem1  33188  elrspunsn  33367  mxidlirredi  33409  1arithidomlem1  33473  1arithidomlem2  33474  1arithidom  33475  dimkerim  33600  lvecendof1f1o  33606  fldextrspunlsplem  33646  nn0constr  33734  constraddcl  33735  constrnegcl  33736  constrremulcl  33740  constrrecl  33742  constrimcl  33743  constrmulcl  33744  constrreinvcl  33745  constrinvcl  33746  constrresqrtcl  33750  constrabscl  33751  2sqr3minply  33753  submatminr1  33783  mdetpmtr1  33796  madjusmdetlem1  33800  zarcmplem  33854  qqhnm  33963  esumfzf  34042  ddemeas  34209  sseqp1  34369  ballotlemi1  34477  ballotlemii  34478  ballotlemic  34481  ballotlem1c  34482  fsum2dsub  34581  circlemeth  34614  hgt750lemb  34630  hgt750lema  34631  hgt750leme  34632  elmrsubrn  35503  cos2h  37601  itg2addnclem  37661  itgmulc2nclem2  37677  areacirclem1  37698  areacirclem4  37701  cntotbnd  37786  atmod2i2  39851  trljat1  40155  trljat2  40156  cdleme9  40242  cdleme15b  40264  cdleme20c  40300  cdleme22eALTN  40334  dvhopN  41105  doca2N  41115  cdlemn10  41195  dochocss  41355  djhlj  41390  dihprrnlem1N  41413  dihprrnlem2  41414  lcfl7lem  41488  lclkrlem2c  41498  hgmapadd  41883  hdmapinvlem3  41909  hgmapvvlem1  41912  sumcubes  42296  zaddcomlem  42446  fidomncyc  42518  selvvvval  42568  rmydbl  42923  jm2.18  42971  jm2.19  42976  proot1hash  43178  dssmapnvod  44003  binomcxplemnotnn0  44339  oddfl  45270  dstregt0  45274  supsubc  45343  absimlere  45468  uzinico2  45552  mccllem  45588  ellimcabssub0  45608  sumnnodd  45621  climresmpt  45650  limsupresuz  45694  liminfresuz  45775  coskpi2  45857  cosknegpi  45860  dvsinax  45904  dvnmptdivc  45929  dvnxpaek  45933  dvnmul  45934  dvmptfprodlem  45935  ditgeqiooicc  45951  itgioocnicc  45968  itgspltprt  45970  wallispi2lem2  46063  dirkerper  46087  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem18  46116  fourierdlem19  46117  fourierdlem33  46131  fourierdlem35  46133  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem53  46150  fourierdlem63  46160  fourierdlem65  46162  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem81  46178  fourierdlem82  46179  fourierdlem83  46180  fourierdlem84  46181  fourierdlem90  46187  fourierdlem93  46190  fourierdlem95  46192  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem111  46208  fourierswlem  46221  fouriersw  46222  etransclem4  46229  etransclem9  46234  etransclem28  46253  etransclem35  46260  etransclem38  46263  sge0tsms  46371  sge0sup  46382  sge0resplit  46397  sge0split  46400  sge0ss  46403  sge0rpcpnf  46412  sge0isum  46418  sge0xadd  46426  sge0seq  46437  ismeannd  46458  caratheodorylem1  46517  isomenndlem  46521  hoicvrrex  46547  ovn0lem  46556  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnlecvr2  46601  voncmpl  46612  hspmbllem1  46617  hspmbllem2  46618  ovolval4lem1  46640  incsmf  46733  smfpimltmpt  46737  smfpimltxrmptf  46749  decsmf  46758  smfpimgtmpt  46772  smfpimgtxrmptf  46775  smfmullem1  46782  smflimsuplem2  46812  sigarac  46843  cevathlem2  46859  m1modmmod  47352  fmtnorec3  47542  fmtnorec4  47543  oddflALTV  47657  perfectALTVlem2  47716  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  uspgrlimlem1  47982  gpgvtxedg0  48057  gpgvtxedg1  48058  gpg3kgrtriexlem2  48078  ply1mulgsum  48385  lindslinindsimp2lem5  48457  nn0sumshdiglemA  48614  nn0sumshdiglemB  48615  nn0sumshdiglem2  48617  itschlc0yqe  48755