Theorem 3eqtrrd 2803

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755

This theorem is used by:  fimacnvinrn  7079  fvcofneq  7101  iunfictbso  10203  axcnre  11259  fseq1p1m1  13742  seqf1olem1  14194  expmulz  14261  expubnd  14331  subsq  14364  bcm1k  14469  bcpasc  14475  cshwcshid  14989  crim  15294  rereb  15299  rlimrecl  15759  iseraltlem2  15862  fsumsplit1  15923  fsumparts  15985  isumshft  16020  geoserg  16047  pwdif  16049  efsub  16280  sincossq  16356  efieq1re  16379  nn0expgcd  16750  eucalg  16774  lcmfunsnlem  16828  phiprmpw  16965  modprmn0modprm0  16997  coprimeprodsq  16998  pythagtriplem15  17019  pythagtriplem17  17021  fldivp1  17087  1arithlem4  17116  setsidvald  17389  setsid  17397  pwsbas  17670  invfuc  18164  estrreslem1  18323  latdisdlem  18682  ghmquskerco  19510  odinv  19787  frgpuplem  19998  gexexlem  20078  fincygsubgodd  20340  srgbinomlem4  20467  gsumdixp  20560  c0snmgmhm  20704  funcrngcsetc  20904  funcringcsetc  20938  cnfldsub  21718  mplcoe1  22358  evlsvarsrng  22428  selvvvval  22463  psdmul  22499  ply1coe  22628  evls1varsrng  22670  mat1scmat  22866  m1detdiag  22924  mdetunilem7  22945  madugsum  22970  pm2mpmhmlem2  23149  mretopd  23422  upxp  23954  uptx  23956  imasdsf1olem  24704  clmvs2  25427  cphipipcj  25533  cphipval2  25574  itgmulc2lem2  26165  r1pid  26491  coeeulem  26555  fta1lem  26640  aaliou3lem8  26684  eff1olem  26888  tanarg  26959  logcnlem4  26985  root1cj  27096  angpieqvdlem  27168  quad2  27179  dcubic  27186  quart1  27196  jensen  27328  lgamgulmlem5  27372  lgamgulm2  27375  ftalem5  27416  basellem8  27427  chpchtsum  27558  logfaclbnd  27561  perfectlem2  27569  gausslemma2dlem1a  27704  2sqlem3  27759  dchrvmasum2lem  27835  dchrvmasumiflem2  27841  selberglem2  27885  selberg3r  27908  pntlem3  27948  ostth2  27976  ostth3  27977  madeoldsuc  28283  zseo  28820  addhalfcut  28857  pw2cut2  28860  krippenlem  29174  colinearalglem1  29496  axlowdimlem16  29547  axcontlem4  29557  clwlkclwwlkfo  30612  nmbdoplbi  32638  nmcopexi  32641  nmbdfnlbi  32663  nmcfnexi  32665  nmcfnlbi  32666  hstoh  32846  fcobij  33365  lt2addrd  33395  xlt2addrd  33404  cshwrnid  33575  symgfcoeu  33696  cycpmconjslem2  33769  cycpmconjs  33770  isarchi3  33801  archirngz  33803  elrgspnsubrunlem1  33861  elrspunsn  34032  mxidlirredi  34049  1arithidomlem1  34120  1arithidomlem2  34121  1arithidom  34122  evlextv  34227  esplyfval1  34258  dimkerim  34312  lvecendof1f1o  34318  fldextrspunlsplem  34358  nn0constr  34446  constraddcl  34447  constrnegcl  34448  constrremulcl  34452  constrrecl  34454  constrimcl  34455  constrmulcl  34456  constrreinvcl  34457  constrinvcl  34458  constrresqrtcl  34462  constrabscl  34463  2sqr3minply  34465  submatminr1  34495  mdetpmtr1  34508  madjusmdetlem1  34512  zarcmplem  34566  qqhnm  34675  esumfzf  34754  ddemeas  34922  sseqp1  35080  ballotlemi1  35188  ballotlemii  35189  ballotlemic  35192  ballotlem1c  35193  fsum2dsub  35289  circlemeth  35322  hgt750lemb  35338  hgt750lema  35339  hgt750leme  35340  elmrsubrn  36406  nadddilem1  37096  cos2h  38674  itg2addnclem  38729  itgmulc2nclem2  38745  areacirclem1  38766  areacirclem4  38769  cntotbnd  38870  atmod2i2  41059  trljat1  41363  trljat2  41364  cdleme9  41450  cdleme15b  41472  cdleme20c  41508  cdleme22eALTN  41542  dvhopN  42313  doca2N  42323  cdlemn10  42403  dochocss  42563  djhlj  42598  dihprrnlem1N  42621  dihprrnlem2  42622  lcfl7lem  42696  lclkrlem2c  42706  hgmapadd  43091  hdmapinvlem3  43117  hgmapvvlem1  43120  sumcubes  43510  zaddcomlem  43667  fidomncyc  43739  rmydbl  44087  jm2.18  44135  jm2.19  44140  proot1hash  44337  dssmapnvod  45160  binomcxplemnotnn0  45480  oddfl  46433  dstregt0  46437  supsubc  46504  absimlere  46628  uzinico2  46712  mccllem  46748  ellimcabssub0  46768  sumnnodd  46781  climresmpt  46808  limsupresuz  46852  liminfresuz  46933  coskpi2  47015  cosknegpi  47018  dvsinax  47062  dvnmptdivc  47087  dvnxpaek  47091  dvnmul  47092  dvmptfprodlem  47093  ditgeqiooicc  47109  itgioocnicc  47126  itgspltprt  47128  wallispi2lem2  47221  dirkerper  47245  dirkertrigeqlem2  47248  dirkertrigeqlem3  47249  dirkertrigeq  47250  dirkercncflem2  47253  dirkercncflem4  47255  fourierdlem18  47274  fourierdlem19  47275  fourierdlem33  47289  fourierdlem35  47291  fourierdlem41  47297  fourierdlem42  47298  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem53  47308  fourierdlem63  47318  fourierdlem65  47320  fourierdlem73  47328  fourierdlem74  47329  fourierdlem75  47330  fourierdlem81  47336  fourierdlem82  47337  fourierdlem83  47338  fourierdlem84  47339  fourierdlem90  47345  fourierdlem93  47348  fourierdlem95  47350  fourierdlem103  47358  fourierdlem104  47359  fourierdlem107  47362  fourierdlem111  47366  fourierswlem  47379  fouriersw  47380  etransclem4  47387  etransclem9  47392  etransclem28  47411  etransclem35  47418  etransclem38  47421  sge0tsms  47529  sge0sup  47540  sge0resplit  47555  sge0split  47558  sge0ss  47561  sge0rpcpnf  47570  sge0isum  47576  sge0xadd  47584  sge0seq  47595  ismeannd  47616  caratheodorylem1  47675  isomenndlem  47679  hoicvrrex  47705  ovn0lem  47714  hoidmvlelem2  47745  hoidmvlelem3  47746  ovnlecvr2  47759  voncmpl  47770  hspmbllem1  47775  hspmbllem2  47776  ovolval4lem1  47798  incsmf  47891  smfpimltmpt  47895  smfpimltxrmptf  47907  decsmf  47916  smfpimgtmpt  47930  smfpimgtxrmptf  47933  smfmullem1  47940  smflimsuplem2  47970  sigarac  48001  cevathlem2  48017  sin3t  48056  cos3t  48057  m1modmmod  48573  fmtnorec3  48772  fmtnorec4  48773  oddflALTV  48900  perfectALTVlem2  48959  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  uspgrlimlem1  49225  gpgvtxedg0  49300  gpgvtxedg1  49301  gpg3kgrtriexlem2  49321  ply1mulgsum  49641  lindslinindsimp2lem5  49713  nn0sumshdiglemA  49870  nn0sumshdiglemB  49871  nn0sumshdiglem2  49873  itschlc0yqe  50011