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 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  dfif5  4504  resindmOLD  6030  difxp1  6162  difxp2  6163  dfdm2  6282  cofunex2g  7943  df1st2  8089  df2nd2  8090  domss2  9120  adderpqlem  10934  dfn2  12512  9p1e10  12708  sqrtm1  15322  0.999...  15931  pockthi  16962  matgsum  22594  indistps  23168  indistps2  23169  refun0  23672  filconn  24040  sincosq3sgn  26665  sincosq4sgn  26666  eff1o  26714  ax5seglem7  29285  0grsubgr  29628  nbupgrres  29714  vtxdginducedm1fi  29894  clwwlknclwwlkdif  30330  cnnvg  31030  cnnvs  31032  cnnvnm  31033  h2hva  31326  h2hsm  31327  h2hnm  31328  hhssva  31609  hhsssm  31610  hhssnm  31611  spansnji  31998  lnopunilem1  32362  lnophmlem2  32369  stadd3i  32600  indifundif  32870  dpmul4  33233  xrsp0  33332  xrsp1  33333  hgt750lemd  35035  hgt750lem  35038  rankeq1o  36663  poimirlem8  38279  mbfposadd  38318  iocunico  43938  corcltrcl  44465  binomcxplemdvsum  45065  cosnegpi  46581  fourierdlem62  46882  fouriersw  46945  salexct3  47056  salgensscntex  47058  caragenuncllem  47226  isomenndlem  47244  goldratmolem2  47623  usgrexmpl2edg  48794