Theorem 3eqtrrd 2776

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  fimacnvinrn  7016  fvcofneq  7038  iunfictbso  10024  axcnre  11075  fseq1p1m1  13514  seqf1olem1  13964  expmulz  14031  expubnd  14101  subsq  14133  bcm1k  14238  bcpasc  14244  cshwcshid  14750  crim  15038  rereb  15043  rlimrecl  15503  iseraltlem2  15606  fsumsplit1  15668  fsumparts  15729  isumshft  15762  geoserg  15789  pwdif  15791  efsub  16025  sincossq  16101  efieq1re  16124  nn0expgcd  16491  eucalg  16514  lcmfunsnlem  16568  phiprmpw  16703  modprmn0modprm0  16735  coprimeprodsq  16736  pythagtriplem15  16757  pythagtriplem17  16759  fldivp1  16825  1arithlem4  16854  setsidvald  17126  setsid  17134  pwsbas  17407  invfuc  17901  estrreslem1  18060  latdisdlem  18419  ghmquskerco  19213  odinv  19490  frgpuplem  19701  gexexlem  19781  fincygsubgodd  20043  srgbinomlem4  20164  gsumdixp  20254  c0snmgmhm  20398  funcrngcsetc  20573  funcringcsetc  20607  cnfldsub  21352  mplcoe1  21992  evlsvarsrng  22062  psdmul  22109  ply1idvr1OLD  22239  ply1coe  22242  evls1varsrng  22284  mat1scmat  22483  m1detdiag  22541  mdetunilem7  22562  madugsum  22587  pm2mpmhmlem2  22763  mretopd  23036  upxp  23567  uptx  23569  imasdsf1olem  24317  clmvs2  25050  cphipipcj  25156  cphipval2  25197  itgmulc2lem2  25790  r1pid  26122  coeeulem  26185  fta1lem  26271  aaliou3lem8  26309  eff1olem  26513  tanarg  26584  logcnlem4  26610  root1cj  26722  angpieqvdlem  26794  quad2  26805  dcubic  26812  quart1  26822  jensen  26955  lgamgulmlem5  26999  lgamgulm2  27002  ftalem5  27043  basellem8  27054  chpchtsum  27186  logfaclbnd  27189  perfectlem2  27197  gausslemma2dlem1a  27332  2sqlem3  27387  dchrvmasum2lem  27463  dchrvmasumiflem2  27469  selberglem2  27513  selberg3r  27536  pntlem3  27576  ostth2  27604  ostth3  27605  madeoldsuc  27881  zseo  28418  addhalfcut  28455  pw2cut2  28458  krippenlem  28762  colinearalglem1  28979  axlowdimlem16  29030  axcontlem4  29040  clwlkclwwlkfo  30084  nmbdoplbi  32099  nmcopexi  32102  nmbdfnlbi  32124  nmcfnexi  32126  nmcfnlbi  32127  hstoh  32307  fcobij  32799  lt2addrd  32830  xlt2addrd  32839  cshwrnid  33043  symgfcoeu  33164  cycpmconjslem2  33237  cycpmconjs  33238  isarchi3  33269  archirngz  33271  elrgspnsubrunlem1  33329  elrspunsn  33510  mxidlirredi  33552  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  evlextv  33707  dimkerim  33784  lvecendof1f1o  33790  fldextrspunlsplem  33830  nn0constr  33918  constraddcl  33919  constrnegcl  33920  constrremulcl  33924  constrrecl  33926  constrimcl  33927  constrmulcl  33928  constrreinvcl  33929  constrinvcl  33930  constrresqrtcl  33934  constrabscl  33935  2sqr3minply  33937  submatminr1  33967  mdetpmtr1  33980  madjusmdetlem1  33984  zarcmplem  34038  qqhnm  34147  esumfzf  34226  ddemeas  34393  sseqp1  34552  ballotlemi1  34660  ballotlemii  34661  ballotlemic  34664  ballotlem1c  34665  fsum2dsub  34764  circlemeth  34797  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  elmrsubrn  35714  cos2h  37812  itg2addnclem  37872  itgmulc2nclem2  37888  areacirclem1  37909  areacirclem4  37912  cntotbnd  37997  atmod2i2  40132  trljat1  40436  trljat2  40437  cdleme9  40523  cdleme15b  40545  cdleme20c  40581  cdleme22eALTN  40615  dvhopN  41386  doca2N  41396  cdlemn10  41476  dochocss  41636  djhlj  41671  dihprrnlem1N  41694  dihprrnlem2  41695  lcfl7lem  41769  lclkrlem2c  41779  hgmapadd  42164  hdmapinvlem3  42190  hgmapvvlem1  42193  sumcubes  42578  zaddcomlem  42728  fidomncyc  42800  selvvvval  42838  rmydbl  43192  jm2.18  43240  jm2.19  43245  proot1hash  43447  dssmapnvod  44271  binomcxplemnotnn0  44607  oddfl  45536  dstregt0  45540  supsubc  45608  absimlere  45733  uzinico2  45817  mccllem  45853  ellimcabssub0  45873  sumnnodd  45886  climresmpt  45913  limsupresuz  45957  liminfresuz  46038  coskpi2  46120  cosknegpi  46123  dvsinax  46167  dvnmptdivc  46192  dvnxpaek  46196  dvnmul  46197  dvmptfprodlem  46198  ditgeqiooicc  46214  itgioocnicc  46231  itgspltprt  46233  wallispi2lem2  46326  dirkerper  46350  dirkertrigeqlem2  46353  dirkertrigeqlem3  46354  dirkertrigeq  46355  dirkercncflem2  46358  dirkercncflem4  46360  fourierdlem18  46379  fourierdlem19  46380  fourierdlem33  46394  fourierdlem35  46396  fourierdlem41  46402  fourierdlem42  46403  fourierdlem48  46408  fourierdlem49  46409  fourierdlem50  46410  fourierdlem53  46413  fourierdlem63  46423  fourierdlem65  46425  fourierdlem73  46433  fourierdlem74  46434  fourierdlem75  46435  fourierdlem81  46441  fourierdlem82  46442  fourierdlem83  46443  fourierdlem84  46444  fourierdlem90  46450  fourierdlem93  46453  fourierdlem95  46455  fourierdlem103  46463  fourierdlem104  46464  fourierdlem107  46467  fourierdlem111  46471  fourierswlem  46484  fouriersw  46485  etransclem4  46492  etransclem9  46497  etransclem28  46516  etransclem35  46523  etransclem38  46526  sge0tsms  46634  sge0sup  46645  sge0resplit  46660  sge0split  46663  sge0ss  46666  sge0rpcpnf  46675  sge0isum  46681  sge0xadd  46689  sge0seq  46700  ismeannd  46721  caratheodorylem1  46780  isomenndlem  46784  hoicvrrex  46810  ovn0lem  46819  hoidmvlelem2  46850  hoidmvlelem3  46851  ovnlecvr2  46864  voncmpl  46875  hspmbllem1  46880  hspmbllem2  46881  ovolval4lem1  46903  incsmf  46996  smfpimltmpt  47000  smfpimltxrmptf  47012  decsmf  47021  smfpimgtmpt  47035  smfpimgtxrmptf  47038  smfmullem1  47045  smflimsuplem2  47075  sigarac  47106  cevathlem2  47122  m1modmmod  47614  fmtnorec3  47804  fmtnorec4  47805  oddflALTV  47919  perfectALTVlem2  47978  nnsum4primeseven  48056  nnsum4primesevenALTV  48057  uspgrlimlem1  48244  gpgvtxedg0  48319  gpgvtxedg1  48320  gpg3kgrtriexlem2  48340  ply1mulgsum  48646  lindslinindsimp2lem5  48718  nn0sumshdiglemA  48875  nn0sumshdiglemB  48876  nn0sumshdiglem2  48878  itschlc0yqe  49016