Theorem 3eqtrri 2764

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

Syntax hints:   = wceq 1541

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  dfif5  4507  resindm  5991  difxp1  6122  difxp2  6123  dfdm2  6238  cofunex2g  7887  df1st2  8035  df2nd2  8036  domss2  9087  adderpqlem  10899  dfn2  12435  9p1e10  12629  sqrtm1  15172  0.999...  15777  pockthi  16790  matgsum  21823  indistps  22398  indistps2  22399  refun0  22903  filconn  23271  sincosq3sgn  25894  sincosq4sgn  25895  eff1o  25942  ax5seglem7  27947  0grsubgr  28289  nbupgrres  28375  vtxdginducedm1fi  28555  clwwlknclwwlkdif  28986  cnnvg  29683  cnnvs  29685  cnnvnm  29686  h2hva  29979  h2hsm  29980  h2hnm  29981  hhssva  30262  hhsssm  30263  hhssnm  30264  spansnji  30651  lnopunilem1  31015  lnophmlem2  31022  stadd3i  31253  indifundif  31516  dpmul4  31840  xrsp0  31942  xrsp1  31943  hgt750lemd  33350  hgt750lem  33353  rankeq1o  34832  poimirlem8  36159  mbfposadd  36198  iocunico  41603  corcltrcl  42133  binomcxplemdvsum  42757  cosnegpi  44228  fourierdlem62  44529  fouriersw  44592  salexct3  44703  salgensscntex  44705  caragenuncllem  44873  isomenndlem  44891