Theorem 3eqtrri 2788

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

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

This theorem is used by:  dfif5  4499  resindmOLD  6024  difxp1  6157  difxp2  6158  dfdm2  6279  cofunex2g  7947  df1st2  8095  df2nd2  8096  domss2  9134  adderpqlem  10963  dfn2  12541  9p1e10  12738  sqrtm1  15362  0.999...  15970  pockthi  16999  matgsum  22659  indistps  23236  indistps2  23237  refun0  23741  filconn  24109  sincosq3sgn  26738  sincosq4sgn  26739  eff1o  26786  ax5seglem7  29392  0grsubgr  29738  nbupgrres  29824  vtxdginducedm1fi  30004  clwwlknclwwlkdif  30449  cnnvg  31159  cnnvs  31161  cnnvnm  31162  h2hva  31455  h2hsm  31456  h2hnm  31457  hhssva  31738  hhsssm  31739  hhssnm  31740  spansnji  32127  lnopunilem1  32491  lnophmlem2  32498  stadd3i  32729  indifundif  32999  dpmul4  33359  xrsp0  33452  xrsp1  33453  hgt750lemd  35156  hgt750lem  35159  rankeq1o  36751  poimirlem8  38377  mbfposadd  38416  iocunico  44052  corcltrcl  44579  binomcxplemdvsum  45179  cosnegpi  46695  fourierdlem62  46996  fouriersw  47059  salexct3  47170  salgensscntex  47172  caragenuncllem  47340  isomenndlem  47358  goldpolyfactor  47745  goldratmolem2  47751  usgrexmpl2edg  48945