Theorem 3eqtrri 2767

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 2762	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2763	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  dfif5  4471  resindm  5982  difxp1  6116  difxp2  6117  dfdm2  6232  cofunex2g  7892  df1st2  8037  df2nd2  8038  domss2  9064  adderpqlem  10868  dfn2  12441  9p1e10  12637  sqrtm1  15228  0.999...  15837  pockthi  16869  matgsum  22420  indistps  22994  indistps2  22995  refun0  23498  filconn  23866  sincosq3sgn  26482  sincosq4sgn  26483  eff1o  26531  ax5seglem7  29022  0grsubgr  29365  nbupgrres  29451  vtxdginducedm1fi  29631  clwwlknclwwlkdif  30067  cnnvg  30767  cnnvs  30769  cnnvnm  30770  h2hva  31063  h2hsm  31064  h2hnm  31065  hhssva  31346  hhsssm  31347  hhssnm  31348  spansnji  31735  lnopunilem1  32099  lnophmlem2  32106  stadd3i  32337  indifundif  32612  dpmul4  32992  xrsp0  33091  xrsp1  33092  hgt750lemd  34832  hgt750lem  34835  rankeq1o  36399  poimirlem8  37995  mbfposadd  38034  iocunico  43656  corcltrcl  44183  binomcxplemdvsum  44799  cosnegpi  46310  fourierdlem62  46611  fouriersw  46674  salexct3  46785  salgensscntex  46787  caragenuncllem  46955  isomenndlem  46973  goldratmolem2  47349  usgrexmpl2edg  48520