Theorem 3eqtrrd 2779

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  fimacnvinrn  7012  fvcofneq  7034  iunfictbso  10027  axcnre  11078  fseq1p1m1  13543  seqf1olem1  13994  expmulz  14061  expubnd  14131  subsq  14163  bcm1k  14268  bcpasc  14274  cshwcshid  14780  crim  15068  rereb  15073  rlimrecl  15533  iseraltlem2  15636  fsumsplit1  15698  fsumparts  15760  isumshft  15795  geoserg  15822  pwdif  15824  efsub  16058  sincossq  16134  efieq1re  16157  nn0expgcd  16524  eucalg  16547  lcmfunsnlem  16601  phiprmpw  16737  modprmn0modprm0  16769  coprimeprodsq  16770  pythagtriplem15  16791  pythagtriplem17  16793  fldivp1  16859  1arithlem4  16888  setsidvald  17160  setsid  17168  pwsbas  17441  invfuc  17935  estrreslem1  18094  latdisdlem  18453  ghmquskerco  19250  odinv  19527  frgpuplem  19738  gexexlem  19818  fincygsubgodd  20080  srgbinomlem4  20201  gsumdixp  20289  c0snmgmhm  20433  funcrngcsetc  20612  funcringcsetc  20646  cnfldsub  21375  mplcoe1  22013  evlsvarsrng  22083  selvvvval  22118  psdmul  22154  ply1idvr1OLD  22281  ply1coe  22284  evls1varsrng  22326  mat1scmat  22522  m1detdiag  22580  mdetunilem7  22601  madugsum  22626  pm2mpmhmlem2  22802  mretopd  23075  upxp  23606  uptx  23608  imasdsf1olem  24356  clmvs2  25079  cphipipcj  25185  cphipval2  25226  itgmulc2lem2  25818  r1pid  26144  coeeulem  26207  fta1lem  26291  aaliou3lem8  26329  eff1olem  26530  tanarg  26601  logcnlem4  26627  root1cj  26738  angpieqvdlem  26810  quad2  26821  dcubic  26828  quart1  26838  jensen  26970  lgamgulmlem5  27014  lgamgulm2  27017  ftalem5  27058  basellem8  27069  chpchtsum  27200  logfaclbnd  27203  perfectlem2  27211  gausslemma2dlem1a  27346  2sqlem3  27401  dchrvmasum2lem  27477  dchrvmasumiflem2  27483  selberglem2  27527  selberg3r  27550  pntlem3  27590  ostth2  27618  ostth3  27619  madeoldsuc  27895  zseo  28432  addhalfcut  28469  pw2cut2  28472  krippenlem  28776  colinearalglem1  28993  axlowdimlem16  29044  axcontlem4  29054  clwlkclwwlkfo  30097  nmbdoplbi  32113  nmcopexi  32116  nmbdfnlbi  32138  nmcfnexi  32140  nmcfnlbi  32141  hstoh  32321  fcobij  32812  lt2addrd  32842  xlt2addrd  32851  cshwrnid  33040  symgfcoeu  33163  cycpmconjslem2  33236  cycpmconjs  33237  isarchi3  33268  archirngz  33270  elrgspnsubrunlem1  33328  elrspunsn  33512  mxidlirredi  33554  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  evlextv  33726  esplyfval1  33757  dimkerim  33811  lvecendof1f1o  33817  fldextrspunlsplem  33857  nn0constr  33945  constraddcl  33946  constrnegcl  33947  constrremulcl  33951  constrrecl  33953  constrimcl  33954  constrmulcl  33955  constrreinvcl  33956  constrinvcl  33957  constrresqrtcl  33961  constrabscl  33962  2sqr3minply  33964  submatminr1  33994  mdetpmtr1  34007  madjusmdetlem1  34011  zarcmplem  34065  qqhnm  34174  esumfzf  34253  ddemeas  34420  sseqp1  34579  ballotlemi1  34687  ballotlemii  34688  ballotlemic  34691  ballotlem1c  34692  fsum2dsub  34791  circlemeth  34824  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  elmrsubrn  35748  cos2h  37978  itg2addnclem  38038  itgmulc2nclem2  38054  areacirclem1  38075  areacirclem4  38078  cntotbnd  38163  atmod2i2  40354  trljat1  40658  trljat2  40659  cdleme9  40745  cdleme15b  40767  cdleme20c  40803  cdleme22eALTN  40837  dvhopN  41608  doca2N  41618  cdlemn10  41698  dochocss  41858  djhlj  41893  dihprrnlem1N  41916  dihprrnlem2  41917  lcfl7lem  41991  lclkrlem2c  42001  hgmapadd  42386  hdmapinvlem3  42412  hgmapvvlem1  42415  sumcubes  42790  zaddcomlem  42953  fidomncyc  43021  rmydbl  43385  jm2.18  43433  jm2.19  43438  proot1hash  43640  dssmapnvod  44464  binomcxplemnotnn0  44800  oddfl  45726  dstregt0  45730  supsubc  45798  absimlere  45922  uzinico2  46006  mccllem  46042  ellimcabssub0  46062  sumnnodd  46075  climresmpt  46102  limsupresuz  46146  liminfresuz  46227  coskpi2  46309  cosknegpi  46312  dvsinax  46356  dvnmptdivc  46381  dvnxpaek  46385  dvnmul  46386  dvmptfprodlem  46387  ditgeqiooicc  46403  itgioocnicc  46420  itgspltprt  46422  wallispi2lem2  46515  dirkerper  46539  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem18  46568  fourierdlem19  46569  fourierdlem33  46583  fourierdlem35  46585  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem53  46602  fourierdlem63  46612  fourierdlem65  46614  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem81  46630  fourierdlem82  46631  fourierdlem83  46632  fourierdlem84  46633  fourierdlem90  46639  fourierdlem93  46642  fourierdlem95  46644  fourierdlem103  46652  fourierdlem104  46653  fourierdlem107  46656  fourierdlem111  46660  fourierswlem  46673  fouriersw  46674  etransclem4  46681  etransclem9  46686  etransclem28  46705  etransclem35  46712  etransclem38  46715  sge0tsms  46823  sge0sup  46834  sge0resplit  46849  sge0split  46852  sge0ss  46855  sge0rpcpnf  46864  sge0isum  46870  sge0xadd  46878  sge0seq  46889  ismeannd  46910  caratheodorylem1  46969  isomenndlem  46973  hoicvrrex  46999  ovn0lem  47008  hoidmvlelem2  47039  hoidmvlelem3  47040  ovnlecvr2  47053  voncmpl  47064  hspmbllem1  47069  hspmbllem2  47070  ovolval4lem1  47092  incsmf  47185  smfpimltmpt  47189  smfpimltxrmptf  47201  decsmf  47210  smfpimgtmpt  47224  smfpimgtxrmptf  47227  smfmullem1  47234  smflimsuplem2  47264  sigarac  47295  cevathlem2  47311  sin3t  47334  cos3t  47335  m1modmmod  47827  fmtnorec3  48026  fmtnorec4  48027  oddflALTV  48154  perfectALTVlem2  48213  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  uspgrlimlem1  48479  gpgvtxedg0  48554  gpgvtxedg1  48555  gpg3kgrtriexlem2  48575  ply1mulgsum  48881  lindslinindsimp2lem5  48953  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem2  49113  itschlc0yqe  49251