Theorem 3eqtrri 2757

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 2752	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2753	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  dfif5  4493  resindm  5981  difxp1  6114  difxp2  6115  dfdm2  6229  cofunex2g  7885  df1st2  8031  df2nd2  8032  domss2  9053  adderpqlem  10848  dfn2  12397  9p1e10  12593  sqrtm1  15182  0.999...  15788  pockthi  16819  matgsum  22322  indistps  22896  indistps2  22897  refun0  23400  filconn  23768  sincosq3sgn  26407  sincosq4sgn  26408  eff1o  26456  ax5seglem7  28880  0grsubgr  29223  nbupgrres  29309  vtxdginducedm1fi  29490  clwwlknclwwlkdif  29923  cnnvg  30622  cnnvs  30624  cnnvnm  30625  h2hva  30918  h2hsm  30919  h2hnm  30920  hhssva  31201  hhsssm  31202  hhssnm  31203  spansnji  31590  lnopunilem1  31954  lnophmlem2  31961  stadd3i  32192  indifundif  32468  dpmul4  32854  xrsp0  32966  xrsp1  32967  hgt750lemd  34616  hgt750lem  34619  rankeq1o  36145  poimirlem8  37608  mbfposadd  37647  iocunico  43184  corcltrcl  43712  binomcxplemdvsum  44328  cosnegpi  45848  fourierdlem62  46149  fouriersw  46212  salexct3  46323  salgensscntex  46325  caragenuncllem  46493  isomenndlem  46511  usgrexmpl2edg  48013