Theorem 3eqtrri 2771

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtri.1	⊢ 𝐴 = 𝐵
3eqtri.2	⊢ 𝐵 = 𝐶
3eqtri.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtrri	⊢ 𝐷 = 𝐴

Proof of Theorem 3eqtrri

Step	Hyp	Ref	Expression
1		3eqtri.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtri 2766	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2767	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  dfif5  4472  resindm  5929  difxp1  6057  difxp2  6058  dfdm2  6173  cofunex2g  7766  df1st2  7909  df2nd2  7910  domss2  8872  adderpqlem  10641  dfn2  12176  9p1e10  12368  sqrtm1  14915  0.999...  15521  pockthi  16536  matgsum  21494  indistps  22069  indistps2  22070  refun0  22574  filconn  22942  sincosq3sgn  25562  sincosq4sgn  25563  eff1o  25610  ax5seglem7  27206  0grsubgr  27548  nbupgrres  27634  vtxdginducedm1fi  27814  clwwlknclwwlkdif  28244  cnnvg  28941  cnnvs  28943  cnnvnm  28944  h2hva  29237  h2hsm  29238  h2hnm  29239  hhssva  29520  hhsssm  29521  hhssnm  29522  spansnji  29909  lnopunilem1  30273  lnophmlem2  30280  stadd3i  30511  indifundif  30774  dpmul4  31090  xrsp0  31192  xrsp1  31193  hgt750lemd  32528  hgt750lem  32531  rankeq1o  34400  poimirlem8  35712  mbfposadd  35751  iocunico  40958  corcltrcl  41236  binomcxplemdvsum  41862  cosnegpi  43298  fourierdlem62  43599  fouriersw  43662  salexct3  43771  salgensscntex  43773  caragenuncllem  43940  isomenndlem  43958