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  4501  resindm  5990  difxp1  6126  difxp2  6127  dfdm2  6242  cofunex2g  7908  df1st2  8054  df2nd2  8055  domss2  9077  adderpqlem  10883  dfn2  12431  9p1e10  12627  sqrtm1  15217  0.999...  15823  pockthi  16854  matgsum  22357  indistps  22931  indistps2  22932  refun0  23435  filconn  23803  sincosq3sgn  26442  sincosq4sgn  26443  eff1o  26491  ax5seglem7  28915  0grsubgr  29258  nbupgrres  29344  vtxdginducedm1fi  29525  clwwlknclwwlkdif  29958  cnnvg  30657  cnnvs  30659  cnnvnm  30660  h2hva  30953  h2hsm  30954  h2hnm  30955  hhssva  31236  hhsssm  31237  hhssnm  31238  spansnji  31625  lnopunilem1  31989  lnophmlem2  31996  stadd3i  32227  indifundif  32503  dpmul4  32884  xrsp0  32996  xrsp1  32997  hgt750lemd  34632  hgt750lem  34635  rankeq1o  36152  poimirlem8  37615  mbfposadd  37654  iocunico  43193  corcltrcl  43721  binomcxplemdvsum  44337  cosnegpi  45858  fourierdlem62  46159  fouriersw  46222  salexct3  46333  salgensscntex  46335  caragenuncllem  46503  isomenndlem  46521  usgrexmpl2edg  48013