Theorem 3eqtrrd 2777

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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  fimacnvinrn  7025  fvcofneq  7047  iunfictbso  10036  axcnre  11087  fseq1p1m1  13526  seqf1olem1  13976  expmulz  14043  expubnd  14113  subsq  14145  bcm1k  14250  bcpasc  14256  cshwcshid  14762  crim  15050  rereb  15055  rlimrecl  15515  iseraltlem2  15618  fsumsplit1  15680  fsumparts  15741  isumshft  15774  geoserg  15801  pwdif  15803  efsub  16037  sincossq  16113  efieq1re  16136  nn0expgcd  16503  eucalg  16526  lcmfunsnlem  16580  phiprmpw  16715  modprmn0modprm0  16747  coprimeprodsq  16748  pythagtriplem15  16769  pythagtriplem17  16771  fldivp1  16837  1arithlem4  16866  setsidvald  17138  setsid  17146  pwsbas  17419  invfuc  17913  estrreslem1  18072  latdisdlem  18431  ghmquskerco  19228  odinv  19505  frgpuplem  19716  gexexlem  19796  fincygsubgodd  20058  srgbinomlem4  20179  gsumdixp  20269  c0snmgmhm  20413  funcrngcsetc  20588  funcringcsetc  20622  cnfldsub  21367  mplcoe1  22007  evlsvarsrng  22077  psdmul  22124  ply1idvr1OLD  22254  ply1coe  22257  evls1varsrng  22299  mat1scmat  22498  m1detdiag  22556  mdetunilem7  22577  madugsum  22602  pm2mpmhmlem2  22778  mretopd  23051  upxp  23582  uptx  23584  imasdsf1olem  24332  clmvs2  25065  cphipipcj  25171  cphipval2  25212  itgmulc2lem2  25805  r1pid  26137  coeeulem  26200  fta1lem  26286  aaliou3lem8  26324  eff1olem  26528  tanarg  26599  logcnlem4  26625  root1cj  26737  angpieqvdlem  26809  quad2  26820  dcubic  26827  quart1  26837  jensen  26970  lgamgulmlem5  27014  lgamgulm2  27017  ftalem5  27058  basellem8  27069  chpchtsum  27201  logfaclbnd  27204  perfectlem2  27212  gausslemma2dlem1a  27347  2sqlem3  27402  dchrvmasum2lem  27478  dchrvmasumiflem2  27484  selberglem2  27528  selberg3r  27551  pntlem3  27591  ostth2  27619  ostth3  27620  madeoldsuc  27896  zseo  28433  addhalfcut  28470  pw2cut2  28473  krippenlem  28778  colinearalglem1  28995  axlowdimlem16  29046  axcontlem4  29056  clwlkclwwlkfo  30100  nmbdoplbi  32116  nmcopexi  32119  nmbdfnlbi  32141  nmcfnexi  32143  nmcfnlbi  32144  hstoh  32324  fcobij  32814  lt2addrd  32845  xlt2addrd  32854  cshwrnid  33058  symgfcoeu  33180  cycpmconjslem2  33253  cycpmconjs  33254  isarchi3  33285  archirngz  33287  elrgspnsubrunlem1  33345  elrspunsn  33526  mxidlirredi  33568  1arithidomlem1  33632  1arithidomlem2  33633  1arithidom  33634  evlextv  33723  esplyfval1  33754  dimkerim  33809  lvecendof1f1o  33815  fldextrspunlsplem  33855  nn0constr  33943  constraddcl  33944  constrnegcl  33945  constrremulcl  33949  constrrecl  33951  constrimcl  33952  constrmulcl  33953  constrreinvcl  33954  constrinvcl  33955  constrresqrtcl  33959  constrabscl  33960  2sqr3minply  33962  submatminr1  33992  mdetpmtr1  34005  madjusmdetlem1  34009  zarcmplem  34063  qqhnm  34172  esumfzf  34251  ddemeas  34418  sseqp1  34577  ballotlemi1  34685  ballotlemii  34686  ballotlemic  34689  ballotlem1c  34690  fsum2dsub  34789  circlemeth  34822  hgt750lemb  34838  hgt750lema  34839  hgt750leme  34840  elmrsubrn  35740  cos2h  37866  itg2addnclem  37926  itgmulc2nclem2  37942  areacirclem1  37963  areacirclem4  37966  cntotbnd  38051  atmod2i2  40242  trljat1  40546  trljat2  40547  cdleme9  40633  cdleme15b  40655  cdleme20c  40691  cdleme22eALTN  40725  dvhopN  41496  doca2N  41506  cdlemn10  41586  dochocss  41746  djhlj  41781  dihprrnlem1N  41804  dihprrnlem2  41805  lcfl7lem  41879  lclkrlem2c  41889  hgmapadd  42274  hdmapinvlem3  42300  hgmapvvlem1  42303  sumcubes  42687  zaddcomlem  42837  fidomncyc  42909  selvvvval  42947  rmydbl  43301  jm2.18  43349  jm2.19  43354  proot1hash  43556  dssmapnvod  44380  binomcxplemnotnn0  44716  oddfl  45644  dstregt0  45648  supsubc  45716  absimlere  45841  uzinico2  45925  mccllem  45961  ellimcabssub0  45981  sumnnodd  45994  climresmpt  46021  limsupresuz  46065  liminfresuz  46146  coskpi2  46228  cosknegpi  46231  dvsinax  46275  dvnmptdivc  46300  dvnxpaek  46304  dvnmul  46305  dvmptfprodlem  46306  ditgeqiooicc  46322  itgioocnicc  46339  itgspltprt  46341  wallispi2lem2  46434  dirkerper  46458  dirkertrigeqlem2  46461  dirkertrigeqlem3  46462  dirkertrigeq  46463  dirkercncflem2  46466  dirkercncflem4  46468  fourierdlem18  46487  fourierdlem19  46488  fourierdlem33  46502  fourierdlem35  46504  fourierdlem41  46510  fourierdlem42  46511  fourierdlem48  46516  fourierdlem49  46517  fourierdlem50  46518  fourierdlem53  46521  fourierdlem63  46531  fourierdlem65  46533  fourierdlem73  46541  fourierdlem74  46542  fourierdlem75  46543  fourierdlem81  46549  fourierdlem82  46550  fourierdlem83  46551  fourierdlem84  46552  fourierdlem90  46558  fourierdlem93  46561  fourierdlem95  46563  fourierdlem103  46571  fourierdlem104  46572  fourierdlem107  46575  fourierdlem111  46579  fourierswlem  46592  fouriersw  46593  etransclem4  46600  etransclem9  46605  etransclem28  46624  etransclem35  46631  etransclem38  46634  sge0tsms  46742  sge0sup  46753  sge0resplit  46768  sge0split  46771  sge0ss  46774  sge0rpcpnf  46783  sge0isum  46789  sge0xadd  46797  sge0seq  46808  ismeannd  46829  caratheodorylem1  46888  isomenndlem  46892  hoicvrrex  46918  ovn0lem  46927  hoidmvlelem2  46958  hoidmvlelem3  46959  ovnlecvr2  46972  voncmpl  46983  hspmbllem1  46988  hspmbllem2  46989  ovolval4lem1  47011  incsmf  47104  smfpimltmpt  47108  smfpimltxrmptf  47120  decsmf  47129  smfpimgtmpt  47143  smfpimgtxrmptf  47146  smfmullem1  47153  smflimsuplem2  47183  sigarac  47214  cevathlem2  47230  m1modmmod  47722  fmtnorec3  47912  fmtnorec4  47913  oddflALTV  48027  perfectALTVlem2  48086  nnsum4primeseven  48164  nnsum4primesevenALTV  48165  uspgrlimlem1  48352  gpgvtxedg0  48427  gpgvtxedg1  48428  gpg3kgrtriexlem2  48448  ply1mulgsum  48754  lindslinindsimp2lem5  48826  nn0sumshdiglemA  48983  nn0sumshdiglemB  48984  nn0sumshdiglem2  48986  itschlc0yqe  49124