Theorem 3eqtrri 2773

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

Syntax hints:   = wceq 1542

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 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  dfif5  4481  resindm  5938  difxp1  6066  difxp2  6067  dfdm2  6182  cofunex2g  7780  df1st2  7923  df2nd2  7924  domss2  8897  adderpqlem  10703  dfn2  12238  9p1e10  12430  sqrtm1  14977  0.999...  15583  pockthi  16598  matgsum  21576  indistps  22151  indistps2  22152  refun0  22656  filconn  23024  sincosq3sgn  25647  sincosq4sgn  25648  eff1o  25695  ax5seglem7  27293  0grsubgr  27635  nbupgrres  27721  vtxdginducedm1fi  27901  clwwlknclwwlkdif  28331  cnnvg  29028  cnnvs  29030  cnnvnm  29031  h2hva  29324  h2hsm  29325  h2hnm  29326  hhssva  29607  hhsssm  29608  hhssnm  29609  spansnji  29996  lnopunilem1  30360  lnophmlem2  30367  stadd3i  30598  indifundif  30861  dpmul4  31176  xrsp0  31278  xrsp1  31279  hgt750lemd  32616  hgt750lem  32619  rankeq1o  34461  poimirlem8  35773  mbfposadd  35812  iocunico  41031  corcltrcl  41309  binomcxplemdvsum  41935  cosnegpi  43371  fourierdlem62  43672  fouriersw  43735  salexct3  43844  salgensscntex  43846  caragenuncllem  44013  isomenndlem  44031