Theorem 3eqtrri 2789

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

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  dfif5  4499  resindmOLD  6020  difxp1  6156  difxp2  6157  dfdm2  6283  cofunex2g  7960  df1st2  8107  df2nd2  8108  domss2  9148  adderpqlem  11032  dfn2  12612  9p1e10  12809  sqrtm1  15435  0.999...  16043  pockthi  17078  matgsum  22745  indistps  23322  indistps2  23323  refun0  23827  filconn  24195  sincosq3sgn  26822  sincosq4sgn  26823  eff1o  26870  ax5seglem7  29506  0grsubgr  29852  nbupgrres  29938  vtxdginducedm1fi  30118  clwwlknclwwlkdif  30563  cnnvg  31273  cnnvs  31275  cnnvnm  31276  h2hva  31569  h2hsm  31570  h2hnm  31571  hhssva  31852  hhsssm  31853  hhssnm  31854  spansnji  32241  lnopunilem1  32605  lnophmlem2  32612  stadd3i  32843  indifundif  33113  dpmul4  33473  xrsp0  33566  xrsp1  33567  hgt750lemd  35270  hgt750lem  35273  rankeq1o  36912  poimirlem8  38526  mbfposadd  38565  iocunico  44197  corcltrcl  44724  binomcxplemdvsum  45324  cosnegpi  46846  fourierdlem62  47147  fouriersw  47210  salexct3  47321  salgensscntex  47323  caragenuncllem  47491  isomenndlem  47509  goldpolyfactor  47896  goldratmolem2  47902  usgrexmpl2edg  49096