Theorem 3eqtrri 2791

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 2786	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2787	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  dfif5  4502  resindmOLD  6038  difxp1  6174  difxp2  6175  dfdm2  6308  cofunex2g  7996  df1st2  8146  df2nd2  8147  domss2  9193  adderpqlem  11078  dfn2  12659  9p1e10  12856  sqrtm1  15485  0.999...  16094  pockthi  17129  matgsum  22807  indistps  23384  indistps2  23385  refun0  23889  filconn  24257  sincosq3sgn  26886  sincosq4sgn  26887  eff1o  26934  ax5seglem7  29570  0grsubgr  29916  nbupgrres  30002  vtxdginducedm1fi  30182  clwwlknclwwlkdif  30627  cnnvg  31337  cnnvs  31339  cnnvnm  31340  h2hva  31633  h2hsm  31634  h2hnm  31635  hhssva  31916  hhsssm  31917  hhssnm  31918  spansnji  32305  lnopunilem1  32669  lnophmlem2  32676  stadd3i  32907  indifundif  33219  dpmul4  33576  xrsp0  33672  xrsp1  33673  hgt750lemd  35388  hgt750lem  35391  rankeq1o  37147  poimirlem8  38814  mbfposadd  38853  iocunico  44474  corcltrcl  45000  binomcxplemdvsum  45600  cosnegpi  47150  fourierdlem62  47451  fouriersw  47514  salexct3  47625  salgensscntex  47627  caragenuncllem  47795  isomenndlem  47813  goldpolyfactor  48200  goldratmolem2  48206  usgrexmpl2edg  49400