Theorem 3eqtrri 2793

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 2788	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2789	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 2156  ax-ext 2737

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

This theorem is used by:  dfif5  4506  resindmOLD  6032  difxp1  6164  difxp2  6165  dfdm2  6286  cofunex2g  7953  df1st2  8099  df2nd2  8100  domss2  9131  adderpqlem  10954  dfn2  12532  9p1e10  12729  sqrtm1  15350  0.999...  15958  pockthi  16989  matgsum  22644  indistps  23218  indistps2  23219  refun0  23723  filconn  24091  sincosq3sgn  26716  sincosq4sgn  26717  eff1o  26765  ax5seglem7  29340  0grsubgr  29686  nbupgrres  29772  vtxdginducedm1fi  29952  clwwlknclwwlkdif  30397  cnnvg  31101  cnnvs  31103  cnnvnm  31104  h2hva  31397  h2hsm  31398  h2hnm  31399  hhssva  31680  hhsssm  31681  hhssnm  31682  spansnji  32069  lnopunilem1  32433  lnophmlem2  32440  stadd3i  32671  indifundif  32941  dpmul4  33303  xrsp0  33396  xrsp1  33397  hgt750lemd  35100  hgt750lem  35103  rankeq1o  36700  poimirlem8  38336  mbfposadd  38375  iocunico  43996  corcltrcl  44523  binomcxplemdvsum  45123  cosnegpi  46639  fourierdlem62  46940  fouriersw  47003  salexct3  47114  salgensscntex  47116  caragenuncllem  47284  isomenndlem  47302  goldratmolem2  47681  usgrexmpl2edg  48852