Theorem 3eqtrri 2766

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 2761	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2762	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  dfif5  4545  resindm  6031  difxp1  6165  difxp2  6166  dfdm2  6281  cofunex2g  7936  df1st2  8084  df2nd2  8085  domss2  9136  adderpqlem  10949  dfn2  12485  9p1e10  12679  sqrtm1  15222  0.999...  15827  pockthi  16840  matgsum  21939  indistps  22514  indistps2  22515  refun0  23019  filconn  23387  sincosq3sgn  26010  sincosq4sgn  26011  eff1o  26058  ax5seglem7  28224  0grsubgr  28566  nbupgrres  28652  vtxdginducedm1fi  28832  clwwlknclwwlkdif  29263  cnnvg  29962  cnnvs  29964  cnnvnm  29965  h2hva  30258  h2hsm  30259  h2hnm  30260  hhssva  30541  hhsssm  30542  hhssnm  30543  spansnji  30930  lnopunilem1  31294  lnophmlem2  31301  stadd3i  31532  indifundif  31793  dpmul4  32111  xrsp0  32213  xrsp1  32214  hgt750lemd  33691  hgt750lem  33694  rankeq1o  35174  poimirlem8  36544  mbfposadd  36583  iocunico  42008  corcltrcl  42538  binomcxplemdvsum  43162  cosnegpi  44631  fourierdlem62  44932  fouriersw  44995  salexct3  45106  salgensscntex  45108  caragenuncllem  45276  isomenndlem  45294