Theorem 3eqtrri 2762

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 2757	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2758	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 2706

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

This theorem is referenced by:  dfif5  4515  resindm  6014  difxp1  6151  difxp2  6152  dfdm2  6267  cofunex2g  7942  df1st2  8091  df2nd2  8092  domss2  9144  adderpqlem  10960  dfn2  12506  9p1e10  12702  sqrtm1  15281  0.999...  15884  pockthi  16912  matgsum  22360  indistps  22934  indistps2  22935  refun0  23438  filconn  23806  sincosq3sgn  26445  sincosq4sgn  26446  eff1o  26494  ax5seglem7  28846  0grsubgr  29189  nbupgrres  29275  vtxdginducedm1fi  29456  clwwlknclwwlkdif  29892  cnnvg  30591  cnnvs  30593  cnnvnm  30594  h2hva  30887  h2hsm  30888  h2hnm  30889  hhssva  31170  hhsssm  31171  hhssnm  31172  spansnji  31559  lnopunilem1  31923  lnophmlem2  31930  stadd3i  32161  indifundif  32437  dpmul4  32806  xrsp0  32923  xrsp1  32924  hgt750lemd  34601  hgt750lem  34604  rankeq1o  36110  poimirlem8  37573  mbfposadd  37612  iocunico  43160  corcltrcl  43688  binomcxplemdvsum  44305  cosnegpi  45826  fourierdlem62  46127  fouriersw  46190  salexct3  46301  salgensscntex  46303  caragenuncllem  46471  isomenndlem  46489  usgrexmpl2edg  47933