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 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  fimacnvinrn  7066  fvcofneq  7088  iunfictbso  10094  axcnre  11144  fseq1p1m1  13622  seqf1olem1  14073  expmulz  14140  expubnd  14210  subsq  14242  bcm1k  14347  bcpasc  14353  cshwcshid  14860  crim  15162  rereb  15167  rlimrecl  15627  iseraltlem2  15730  fsumsplit1  15792  fsumparts  15854  isumshft  15889  geoserg  15916  pwdif  15918  efsub  16151  sincossq  16227  efieq1re  16250  nn0expgcd  16617  eucalg  16640  lcmfunsnlem  16694  phiprmpw  16830  modprmn0modprm0  16862  coprimeprodsq  16863  pythagtriplem15  16884  pythagtriplem17  16886  fldivp1  16952  1arithlem4  16981  setsidvald  17254  setsid  17262  pwsbas  17535  invfuc  18029  estrreslem1  18188  latdisdlem  18547  ghmquskerco  19349  odinv  19626  frgpuplem  19837  gexexlem  19917  fincygsubgodd  20179  srgbinomlem4  20306  gsumdixp  20396  c0snmgmhm  20540  funcrngcsetc  20739  funcringcsetc  20773  cnfldsub  21550  mplcoe1  22188  evlsvarsrng  22258  selvvvval  22293  psdmul  22329  ply1coe  22458  evls1varsrng  22500  mat1scmat  22696  m1detdiag  22754  mdetunilem7  22775  madugsum  22800  pm2mpmhmlem2  22976  mretopd  23249  upxp  23780  uptx  23782  imasdsf1olem  24530  clmvs2  25253  cphipipcj  25359  cphipval2  25400  itgmulc2lem2  25992  r1pid  26318  coeeulem  26381  fta1lem  26468  aaliou3lem8  26508  eff1olem  26713  tanarg  26784  logcnlem4  26810  root1cj  26921  angpieqvdlem  26993  quad2  27004  dcubic  27011  quart1  27021  jensen  27153  lgamgulmlem5  27197  lgamgulm2  27200  ftalem5  27241  basellem8  27252  chpchtsum  27383  logfaclbnd  27386  perfectlem2  27394  gausslemma2dlem1a  27529  2sqlem3  27584  dchrvmasum2lem  27660  dchrvmasumiflem2  27666  selberglem2  27710  selberg3r  27733  pntlem3  27773  ostth2  27801  ostth3  27802  madeoldsuc  28078  zseo  28615  addhalfcut  28652  pw2cut2  28655  krippenlem  28967  colinearalglem1  29256  axlowdimlem16  29307  axcontlem4  29317  clwlkclwwlkfo  30360  nmbdoplbi  32376  nmcopexi  32379  nmbdfnlbi  32401  nmcfnexi  32403  nmcfnlbi  32404  hstoh  32584  fcobij  33065  lt2addrd  33095  xlt2addrd  33104  cshwrnid  33281  symgfcoeu  33402  cycpmconjslem2  33475  cycpmconjs  33476  isarchi3  33507  archirngz  33509  elrgspnsubrunlem1  33567  elrspunsn  33737  mxidlirredi  33754  1arithidomlem1  33825  1arithidomlem2  33826  1arithidom  33827  evlextv  33932  esplyfval1  33963  dimkerim  34017  lvecendof1f1o  34023  fldextrspunlsplem  34063  nn0constr  34151  constraddcl  34152  constrnegcl  34153  constrremulcl  34157  constrrecl  34159  constrimcl  34160  constrmulcl  34161  constrreinvcl  34162  constrinvcl  34163  constrresqrtcl  34167  constrabscl  34168  2sqr3minply  34170  submatminr1  34200  mdetpmtr1  34213  madjusmdetlem1  34217  zarcmplem  34271  qqhnm  34380  esumfzf  34459  ddemeas  34626  sseqp1  34785  ballotlemi1  34893  ballotlemii  34894  ballotlemic  34897  ballotlem1c  34898  fsum2dsub  34994  circlemeth  35027  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  elmrsubrn  36012  nadddilem1  36712  cos2h  38282  itg2addnclem  38342  itgmulc2nclem2  38358  areacirclem1  38379  areacirclem4  38382  cntotbnd  38467  atmod2i2  40656  trljat1  40960  trljat2  40961  cdleme9  41047  cdleme15b  41069  cdleme20c  41105  cdleme22eALTN  41139  dvhopN  41910  doca2N  41920  cdlemn10  42000  dochocss  42160  djhlj  42195  dihprrnlem1N  42218  dihprrnlem2  42219  lcfl7lem  42293  lclkrlem2c  42303  hgmapadd  42688  hdmapinvlem3  42714  hgmapvvlem1  42717  sumcubes  43094  zaddcomlem  43257  fidomncyc  43323  rmydbl  43687  jm2.18  43735  jm2.19  43740  proot1hash  43942  dssmapnvod  44766  binomcxplemnotnn0  45086  oddfl  46017  dstregt0  46021  supsubc  46089  absimlere  46213  uzinico2  46297  mccllem  46333  ellimcabssub0  46353  sumnnodd  46366  climresmpt  46393  limsupresuz  46437  liminfresuz  46518  coskpi2  46600  cosknegpi  46603  dvsinax  46647  dvnmptdivc  46672  dvnxpaek  46676  dvnmul  46677  dvmptfprodlem  46678  ditgeqiooicc  46694  itgioocnicc  46711  itgspltprt  46713  wallispi2lem2  46806  dirkerper  46830  dirkertrigeqlem2  46833  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem18  46859  fourierdlem19  46860  fourierdlem33  46874  fourierdlem35  46876  fourierdlem41  46882  fourierdlem42  46883  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem53  46893  fourierdlem63  46903  fourierdlem65  46905  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem81  46921  fourierdlem82  46922  fourierdlem83  46923  fourierdlem84  46924  fourierdlem90  46930  fourierdlem93  46933  fourierdlem95  46935  fourierdlem103  46943  fourierdlem104  46944  fourierdlem107  46947  fourierdlem111  46951  fourierswlem  46964  fouriersw  46965  etransclem4  46972  etransclem9  46977  etransclem28  46996  etransclem35  47003  etransclem38  47006  sge0tsms  47114  sge0sup  47125  sge0resplit  47140  sge0split  47143  sge0ss  47146  sge0rpcpnf  47155  sge0isum  47161  sge0xadd  47169  sge0seq  47180  ismeannd  47201  caratheodorylem1  47260  isomenndlem  47264  hoicvrrex  47290  ovn0lem  47299  hoidmvlelem2  47330  hoidmvlelem3  47331  ovnlecvr2  47344  voncmpl  47355  hspmbllem1  47360  hspmbllem2  47361  ovolval4lem1  47383  incsmf  47476  smfpimltmpt  47480  smfpimltxrmptf  47492  decsmf  47501  smfpimgtmpt  47515  smfpimgtxrmptf  47518  smfmullem1  47525  smflimsuplem2  47555  sigarac  47586  cevathlem2  47602  sin3t  47628  cos3t  47629  m1modmmod  48121  fmtnorec3  48320  fmtnorec4  48321  oddflALTV  48448  perfectALTVlem2  48507  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  uspgrlimlem1  48773  gpgvtxedg0  48848  gpgvtxedg1  48849  gpg3kgrtriexlem2  48869  ply1mulgsum  49190  lindslinindsimp2lem5  49262  nn0sumshdiglemA  49419  nn0sumshdiglemB  49420  nn0sumshdiglem2  49422  itschlc0yqe  49560