Theorem 3eqtrri 2764

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

Syntax hints:   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  dfif5  4496  resindm  5989  difxp1  6123  difxp2  6124  dfdm2  6239  cofunex2g  7894  df1st2  8040  df2nd2  8041  domss2  9064  adderpqlem  10865  dfn2  12414  9p1e10  12609  sqrtm1  15198  0.999...  15804  pockthi  16835  matgsum  22381  indistps  22955  indistps2  22956  refun0  23459  filconn  23827  sincosq3sgn  26465  sincosq4sgn  26466  eff1o  26514  ax5seglem7  29008  0grsubgr  29351  nbupgrres  29437  vtxdginducedm1fi  29618  clwwlknclwwlkdif  30054  cnnvg  30753  cnnvs  30755  cnnvnm  30756  h2hva  31049  h2hsm  31050  h2hnm  31051  hhssva  31332  hhsssm  31333  hhssnm  31334  spansnji  31721  lnopunilem1  32085  lnophmlem2  32092  stadd3i  32323  indifundif  32599  dpmul4  32995  xrsp0  33094  xrsp1  33095  hgt750lemd  34805  hgt750lem  34808  rankeq1o  36365  poimirlem8  37829  mbfposadd  37868  iocunico  43453  corcltrcl  43980  binomcxplemdvsum  44596  cosnegpi  46111  fourierdlem62  46412  fouriersw  46475  salexct3  46586  salgensscntex  46588  caragenuncllem  46756  isomenndlem  46774  usgrexmpl2edg  48275