Theorem 3eqtrri 2826

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

Syntax hints:   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  dfif5  4441  resindm  5867  difxp1  5989  difxp2  5990  dfdm2  6100  cofunex2g  7633  df1st2  7776  df2nd2  7777  domss2  8660  adderpqlem  10365  dfn2  11898  9p1e10  12088  sqrtm1  14627  0.999...  15229  pockthi  16233  matgsum  21042  indistps  21616  indistps2  21617  refun0  22120  filconn  22488  sincosq3sgn  25093  sincosq4sgn  25094  eff1o  25141  ax5seglem7  26729  0grsubgr  27068  nbupgrres  27154  vtxdginducedm1fi  27334  clwwlknclwwlkdif  27764  cnnvg  28461  cnnvs  28463  cnnvnm  28464  h2hva  28757  h2hsm  28758  h2hnm  28759  hhssva  29040  hhsssm  29041  hhssnm  29042  spansnji  29429  lnopunilem1  29793  lnophmlem2  29800  stadd3i  30031  indifundif  30297  dpmul4  30616  xrsp0  30715  xrsp1  30716  hgt750lemd  32029  hgt750lem  32032  rankeq1o  33745  poimirlem8  35065  mbfposadd  35104  iocunico  40161  corcltrcl  40440  binomcxplemdvsum  41059  cosnegpi  42509  fourierdlem62  42810  fouriersw  42873  salexct3  42982  salgensscntex  42984  caragenuncllem  43151  isomenndlem  43169