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  4505  resindm  6001  difxp1  6138  difxp2  6139  dfdm2  6254  cofunex2g  7928  df1st2  8077  df2nd2  8078  domss2  9100  adderpqlem  10907  dfn2  12455  9p1e10  12651  sqrtm1  15241  0.999...  15847  pockthi  16878  matgsum  22324  indistps  22898  indistps2  22899  refun0  23402  filconn  23770  sincosq3sgn  26409  sincosq4sgn  26410  eff1o  26458  ax5seglem7  28862  0grsubgr  29205  nbupgrres  29291  vtxdginducedm1fi  29472  clwwlknclwwlkdif  29908  cnnvg  30607  cnnvs  30609  cnnvnm  30610  h2hva  30903  h2hsm  30904  h2hnm  30905  hhssva  31186  hhsssm  31187  hhssnm  31188  spansnji  31575  lnopunilem1  31939  lnophmlem2  31946  stadd3i  32177  indifundif  32453  dpmul4  32834  xrsp0  32950  xrsp1  32951  hgt750lemd  34639  hgt750lem  34642  rankeq1o  36159  poimirlem8  37622  mbfposadd  37661  iocunico  43200  corcltrcl  43728  binomcxplemdvsum  44344  cosnegpi  45865  fourierdlem62  46166  fouriersw  46229  salexct3  46340  salgensscntex  46342  caragenuncllem  46510  isomenndlem  46528  usgrexmpl2edg  48020