Theorem 3eqtrri 2759

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 2754	. 2 ⊢ 𝐴 = 𝐶
4		3eqtri.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2755	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  dfif5  4489  resindm  5978  difxp1  6112  difxp2  6113  dfdm2  6228  cofunex2g  7882  df1st2  8028  df2nd2  8029  domss2  9049  adderpqlem  10845  dfn2  12394  9p1e10  12590  sqrtm1  15182  0.999...  15788  pockthi  16819  matgsum  22352  indistps  22926  indistps2  22927  refun0  23430  filconn  23798  sincosq3sgn  26436  sincosq4sgn  26437  eff1o  26485  ax5seglem7  28913  0grsubgr  29256  nbupgrres  29342  vtxdginducedm1fi  29523  clwwlknclwwlkdif  29959  cnnvg  30658  cnnvs  30660  cnnvnm  30661  h2hva  30954  h2hsm  30955  h2hnm  30956  hhssva  31237  hhsssm  31238  hhssnm  31239  spansnji  31626  lnopunilem1  31990  lnophmlem2  31997  stadd3i  32228  indifundif  32504  dpmul4  32894  xrsp0  32993  xrsp1  32994  hgt750lemd  34661  hgt750lem  34664  rankeq1o  36213  poimirlem8  37676  mbfposadd  37715  iocunico  43252  corcltrcl  43780  binomcxplemdvsum  44396  cosnegpi  45913  fourierdlem62  46214  fouriersw  46277  salexct3  46388  salgensscntex  46390  caragenuncllem  46558  isomenndlem  46576  usgrexmpl2edg  48068