Theorem 3eqtrri 2769

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 2764	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2765	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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728

This theorem is referenced by:  dfif5  4541  resindm  6047  difxp1  6184  difxp2  6185  dfdm2  6300  cofunex2g  7975  df1st2  8124  df2nd2  8125  domss2  9177  adderpqlem  10995  dfn2  12541  9p1e10  12737  sqrtm1  15315  0.999...  15918  pockthi  16946  matgsum  22444  indistps  23019  indistps2  23020  refun0  23524  filconn  23892  sincosq3sgn  26543  sincosq4sgn  26544  eff1o  26592  ax5seglem7  28951  0grsubgr  29296  nbupgrres  29382  vtxdginducedm1fi  29563  clwwlknclwwlkdif  29999  cnnvg  30698  cnnvs  30700  cnnvnm  30701  h2hva  30994  h2hsm  30995  h2hnm  30996  hhssva  31277  hhsssm  31278  hhssnm  31279  spansnji  31666  lnopunilem1  32030  lnophmlem2  32037  stadd3i  32268  indifundif  32544  dpmul4  32897  xrsp0  33015  xrsp1  33016  hgt750lemd  34664  hgt750lem  34667  rankeq1o  36173  poimirlem8  37636  mbfposadd  37675  iocunico  43228  corcltrcl  43757  binomcxplemdvsum  44379  cosnegpi  45887  fourierdlem62  46188  fouriersw  46251  salexct3  46362  salgensscntex  46364  caragenuncllem  46532  isomenndlem  46550  usgrexmpl2edg  47993