Theorem 3eqtrri 2771

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

Syntax hints:   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  dfif5  4475  resindm  5940  difxp1  6068  difxp2  6069  dfdm2  6184  cofunex2g  7792  df1st2  7938  df2nd2  7939  domss2  8923  adderpqlem  10710  dfn2  12246  9p1e10  12439  sqrtm1  14987  0.999...  15593  pockthi  16608  matgsum  21586  indistps  22161  indistps2  22162  refun0  22666  filconn  23034  sincosq3sgn  25657  sincosq4sgn  25658  eff1o  25705  ax5seglem7  27303  0grsubgr  27645  nbupgrres  27731  vtxdginducedm1fi  27911  clwwlknclwwlkdif  28343  cnnvg  29040  cnnvs  29042  cnnvnm  29043  h2hva  29336  h2hsm  29337  h2hnm  29338  hhssva  29619  hhsssm  29620  hhssnm  29621  spansnji  30008  lnopunilem1  30372  lnophmlem2  30379  stadd3i  30610  indifundif  30873  dpmul4  31188  xrsp0  31290  xrsp1  31291  hgt750lemd  32628  hgt750lem  32631  rankeq1o  34473  poimirlem8  35785  mbfposadd  35824  iocunico  41042  corcltrcl  41347  binomcxplemdvsum  41973  cosnegpi  43408  fourierdlem62  43709  fouriersw  43772  salexct3  43881  salgensscntex  43883  caragenuncllem  44050  isomenndlem  44068