Theorem 3eqtrri 2761

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

Syntax hints:   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720

This theorem is referenced by:  dfif5  4540  resindm  6028  difxp1  6163  difxp2  6164  dfdm2  6279  cofunex2g  7947  df1st2  8097  df2nd2  8098  domss2  9154  adderpqlem  10971  dfn2  12509  9p1e10  12703  sqrtm1  15248  0.999...  15853  pockthi  16869  matgsum  22332  indistps  22907  indistps2  22908  refun0  23412  filconn  23780  sincosq3sgn  26428  sincosq4sgn  26429  eff1o  26476  ax5seglem7  28739  0grsubgr  29084  nbupgrres  29170  vtxdginducedm1fi  29351  clwwlknclwwlkdif  29782  cnnvg  30481  cnnvs  30483  cnnvnm  30484  h2hva  30777  h2hsm  30778  h2hnm  30779  hhssva  31060  hhsssm  31061  hhssnm  31062  spansnji  31449  lnopunilem1  31813  lnophmlem2  31820  stadd3i  32051  indifundif  32314  dpmul4  32631  xrsp0  32733  xrsp1  32734  hgt750lemd  34274  hgt750lem  34277  rankeq1o  35761  poimirlem8  37095  mbfposadd  37134  iocunico  42633  corcltrcl  43163  binomcxplemdvsum  43786  cosnegpi  45249  fourierdlem62  45550  fouriersw  45613  salexct3  45724  salgensscntex  45726  caragenuncllem  45894  isomenndlem  45912