Theorem 3eqtrrd 2809

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  fimacnvinrn  7067  fvcofneq  7089  iunfictbso  10098  axcnre  11149  fseq1p1m1  13626  seqf1olem1  14077  expmulz  14144  expubnd  14214  subsq  14246  bcm1k  14351  bcpasc  14357  cshwcshid  14864  crim  15166  rereb  15171  rlimrecl  15631  iseraltlem2  15734  fsumsplit1  15796  fsumparts  15858  isumshft  15893  geoserg  15920  pwdif  15922  efsub  16156  sincossq  16232  efieq1re  16255  nn0expgcd  16622  eucalg  16645  lcmfunsnlem  16699  phiprmpw  16835  modprmn0modprm0  16867  coprimeprodsq  16868  pythagtriplem15  16889  pythagtriplem17  16891  fldivp1  16957  1arithlem4  16986  setsidvald  17259  setsid  17267  pwsbas  17540  invfuc  18034  estrreslem1  18193  latdisdlem  18552  ghmquskerco  19354  odinv  19631  frgpuplem  19842  gexexlem  19922  fincygsubgodd  20184  srgbinomlem4  20311  gsumdixp  20400  c0snmgmhm  20544  funcrngcsetc  20725  funcringcsetc  20759  cnfldsub  21519  mplcoe1  22157  evlsvarsrng  22227  selvvvval  22262  psdmul  22298  ply1coe  22427  evls1varsrng  22469  mat1scmat  22665  m1detdiag  22723  mdetunilem7  22744  madugsum  22769  pm2mpmhmlem2  22945  mretopd  23218  upxp  23749  uptx  23751  imasdsf1olem  24499  clmvs2  25222  cphipipcj  25328  cphipval2  25369  itgmulc2lem2  25961  r1pid  26287  coeeulem  26350  fta1lem  26437  aaliou3lem8  26475  eff1olem  26679  tanarg  26750  logcnlem4  26776  root1cj  26887  angpieqvdlem  26959  quad2  26970  dcubic  26977  quart1  26987  jensen  27119  lgamgulmlem5  27163  lgamgulm2  27166  ftalem5  27207  basellem8  27218  chpchtsum  27349  logfaclbnd  27352  perfectlem2  27360  gausslemma2dlem1a  27495  2sqlem3  27550  dchrvmasum2lem  27626  dchrvmasumiflem2  27632  selberglem2  27676  selberg3r  27699  pntlem3  27739  ostth2  27767  ostth3  27768  madeoldsuc  28044  zseo  28581  addhalfcut  28618  pw2cut2  28621  krippenlem  28929  colinearalglem1  29197  axlowdimlem16  29248  axcontlem4  29258  clwlkclwwlkfo  30301  nmbdoplbi  32317  nmcopexi  32320  nmbdfnlbi  32342  nmcfnexi  32344  nmcfnlbi  32345  hstoh  32525  fcobij  33006  lt2addrd  33036  xlt2addrd  33045  cshwrnid  33222  symgfcoeu  33343  cycpmconjslem2  33416  cycpmconjs  33417  isarchi3  33448  archirngz  33450  elrgspnsubrunlem1  33508  elrspunsn  33681  mxidlirredi  33699  1arithidomlem1  33770  1arithidomlem2  33771  1arithidom  33772  evlextv  33877  esplyfval1  33908  dimkerim  33962  lvecendof1f1o  33968  fldextrspunlsplem  34008  nn0constr  34096  constraddcl  34097  constrnegcl  34098  constrremulcl  34102  constrrecl  34104  constrimcl  34105  constrmulcl  34106  constrreinvcl  34107  constrinvcl  34108  constrresqrtcl  34112  constrabscl  34113  2sqr3minply  34115  submatminr1  34145  mdetpmtr1  34158  madjusmdetlem1  34162  zarcmplem  34216  qqhnm  34325  esumfzf  34404  ddemeas  34571  sseqp1  34730  ballotlemi1  34838  ballotlemii  34839  ballotlemic  34842  ballotlem1c  34843  fsum2dsub  34939  circlemeth  34972  hgt750lemb  34988  hgt750lema  34989  hgt750leme  34990  elmrsubrn  35911  cos2h  38150  itg2addnclem  38210  itgmulc2nclem2  38226  areacirclem1  38247  areacirclem4  38250  cntotbnd  38335  atmod2i2  40526  trljat1  40830  trljat2  40831  cdleme9  40917  cdleme15b  40939  cdleme20c  40975  cdleme22eALTN  41009  dvhopN  41780  doca2N  41790  cdlemn10  41870  dochocss  42030  djhlj  42065  dihprrnlem1N  42088  dihprrnlem2  42089  lcfl7lem  42163  lclkrlem2c  42173  hgmapadd  42558  hdmapinvlem3  42584  hgmapvvlem1  42587  sumcubes  42964  zaddcomlem  43127  fidomncyc  43195  rmydbl  43559  jm2.18  43607  jm2.19  43612  proot1hash  43814  dssmapnvod  44638  binomcxplemnotnn0  44958  oddfl  45889  dstregt0  45893  supsubc  45961  absimlere  46085  uzinico2  46169  mccllem  46205  ellimcabssub0  46225  sumnnodd  46238  climresmpt  46265  limsupresuz  46309  liminfresuz  46390  coskpi2  46472  cosknegpi  46475  dvsinax  46519  dvnmptdivc  46544  dvnxpaek  46548  dvnmul  46549  dvmptfprodlem  46550  ditgeqiooicc  46566  itgioocnicc  46583  itgspltprt  46585  wallispi2lem2  46678  dirkerper  46702  dirkertrigeqlem2  46705  dirkertrigeqlem3  46706  dirkertrigeq  46707  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem18  46731  fourierdlem19  46732  fourierdlem33  46746  fourierdlem35  46748  fourierdlem41  46754  fourierdlem42  46755  fourierdlem48  46760  fourierdlem49  46761  fourierdlem50  46762  fourierdlem53  46765  fourierdlem63  46775  fourierdlem65  46777  fourierdlem73  46785  fourierdlem74  46786  fourierdlem75  46787  fourierdlem81  46793  fourierdlem82  46794  fourierdlem83  46795  fourierdlem84  46796  fourierdlem90  46802  fourierdlem93  46805  fourierdlem95  46807  fourierdlem103  46815  fourierdlem104  46816  fourierdlem107  46819  fourierdlem111  46823  fourierswlem  46836  fouriersw  46837  etransclem4  46844  etransclem9  46849  etransclem28  46868  etransclem35  46875  etransclem38  46878  sge0tsms  46986  sge0sup  46997  sge0resplit  47012  sge0split  47015  sge0ss  47018  sge0rpcpnf  47027  sge0isum  47033  sge0xadd  47041  sge0seq  47052  ismeannd  47073  caratheodorylem1  47132  isomenndlem  47136  hoicvrrex  47162  ovn0lem  47171  hoidmvlelem2  47202  hoidmvlelem3  47203  ovnlecvr2  47216  voncmpl  47227  hspmbllem1  47232  hspmbllem2  47233  ovolval4lem1  47255  incsmf  47348  smfpimltmpt  47352  smfpimltxrmptf  47364  decsmf  47373  smfpimgtmpt  47387  smfpimgtxrmptf  47390  smfmullem1  47397  smflimsuplem2  47427  sigarac  47458  cevathlem2  47474  sin3t  47497  cos3t  47498  m1modmmod  47990  fmtnorec3  48189  fmtnorec4  48190  oddflALTV  48317  perfectALTVlem2  48376  nnsum4primeseven  48454  nnsum4primesevenALTV  48455  uspgrlimlem1  48642  gpgvtxedg0  48717  gpgvtxedg1  48718  gpg3kgrtriexlem2  48738  ply1mulgsum  49055  lindslinindsimp2lem5  49127  nn0sumshdiglemA  49284  nn0sumshdiglemB  49285  nn0sumshdiglem2  49287  itschlc0yqe  49425