Theorem 3eqtrri 2851

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

Syntax hints:   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  dfif5  4485  resindm  5902  difxp1  6024  difxp2  6025  dfdm2  6134  cofunex2g  7653  df1st2  7795  df2nd2  7796  domss2  8678  adderpqlem  10378  dfn2  11913  9p1e10  12103  sqrtm1  14637  0.999...  15239  pockthi  16245  matgsum  21048  indistps  21621  indistps2  21622  refun0  22125  filconn  22493  sincosq3sgn  25088  sincosq4sgn  25089  eff1o  25135  ax5seglem7  26723  0grsubgr  27062  nbupgrres  27148  vtxdginducedm1fi  27328  clwwlknclwwlkdif  27759  cnnvg  28457  cnnvs  28459  cnnvnm  28460  h2hva  28753  h2hsm  28754  h2hnm  28755  hhssva  29036  hhsssm  29037  hhssnm  29038  spansnji  29425  lnopunilem1  29789  lnophmlem2  29796  stadd3i  30027  indifundif  30287  dpmul4  30592  xrsp0  30670  xrsp1  30671  hgt750lemd  31921  hgt750lem  31924  rankeq1o  33634  poimirlem8  34902  mbfposadd  34941  iocunico  39824  corcltrcl  40091  binomcxplemdvsum  40694  cosnegpi  42155  fourierdlem62  42460  fouriersw  42523  salexct3  42632  salgensscntex  42634  caragenuncllem  42801  isomenndlem  42819