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 1540

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  dfif5  4544  resindm  6030  difxp1  6164  difxp2  6165  dfdm2  6280  cofunex2g  7939  df1st2  8087  df2nd2  8088  domss2  9139  adderpqlem  10952  dfn2  12490  9p1e10  12684  sqrtm1  15227  0.999...  15832  pockthi  16845  matgsum  22160  indistps  22735  indistps2  22736  refun0  23240  filconn  23608  sincosq3sgn  26247  sincosq4sgn  26248  eff1o  26295  ax5seglem7  28461  0grsubgr  28803  nbupgrres  28889  vtxdginducedm1fi  29069  clwwlknclwwlkdif  29500  cnnvg  30199  cnnvs  30201  cnnvnm  30202  h2hva  30495  h2hsm  30496  h2hnm  30497  hhssva  30778  hhsssm  30779  hhssnm  30780  spansnji  31167  lnopunilem1  31531  lnophmlem2  31538  stadd3i  31769  indifundif  32030  dpmul4  32348  xrsp0  32450  xrsp1  32451  hgt750lemd  33959  hgt750lem  33962  rankeq1o  35448  poimirlem8  36800  mbfposadd  36839  iocunico  42263  corcltrcl  42793  binomcxplemdvsum  43417  cosnegpi  44882  fourierdlem62  45183  fouriersw  45246  salexct3  45357  salgensscntex  45359  caragenuncllem  45527  isomenndlem  45545