Theorem 3eqtrri 2807

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

Syntax hints:   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771

This theorem is referenced by:  dfif5  4367  resindm  5747  difxp1  5864  difxp2  5865  dfdm2  5972  cofunex2g  7465  df1st2  7603  df2nd2  7604  domss2  8474  adderpqlem  10176  dfn2  11725  9p1e10  11916  sqrtm1  14499  0.999...  15100  pockthi  16102  matgsum  20753  indistps  21326  indistps2  21327  refun0  21830  filconn  22198  sincosq3sgn  24792  sincosq4sgn  24793  eff1o  24837  ax5seglem7  26427  0grsubgr  26766  nbupgrres  26852  vtxdginducedm1fi  27032  clwwlknclwwlkdif  27488  cnnvg  28235  cnnvs  28237  cnnvnm  28238  h2hva  28533  h2hsm  28534  h2hnm  28535  hhssva  28816  hhsssm  28817  hhssnm  28818  spansnji  29207  lnopunilem1  29571  lnophmlem2  29578  stadd3i  29809  indifundif  30062  dpmul4  30339  xrsp0  30400  xrsp1  30401  hgt750lemd  31567  hgt750lem  31570  rankeq1o  33153  poimirlem8  34341  mbfposadd  34380  iocunico  39213  corcltrcl  39447  binomcxplemdvsum  40103  cosnegpi  41579  fourierdlem62  41885  fouriersw  41948  salexct3  42057  salgensscntex  42059  caragenuncllem  42226  isomenndlem  42244