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  22300  indistps  22874  indistps2  22875  refun0  23378  filconn  23746  sincosq3sgn  26385  sincosq4sgn  26386  eff1o  26434  ax5seglem7  28838  0grsubgr  29181  nbupgrres  29267  vtxdginducedm1fi  29448  clwwlknclwwlkdif  29881  cnnvg  30580  cnnvs  30582  cnnvnm  30583  h2hva  30876  h2hsm  30877  h2hnm  30878  hhssva  31159  hhsssm  31160  hhssnm  31161  spansnji  31548  lnopunilem1  31912  lnophmlem2  31919  stadd3i  32150  indifundif  32426  dpmul4  32807  xrsp0  32923  xrsp1  32924  hgt750lemd  34612  hgt750lem  34615  rankeq1o  36132  poimirlem8  37595  mbfposadd  37634  iocunico  43173  corcltrcl  43701  binomcxplemdvsum  44317  cosnegpi  45838  fourierdlem62  46139  fouriersw  46202  salexct3  46313  salgensscntex  46315  caragenuncllem  46483  isomenndlem  46501  usgrexmpl2edg  47993