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 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728

This theorem is referenced by:  dfif5  4522  resindm  6022  difxp1  6159  difxp2  6160  dfdm2  6275  cofunex2g  7953  df1st2  8102  df2nd2  8103  domss2  9155  adderpqlem  10973  dfn2  12519  9p1e10  12715  sqrtm1  15299  0.999...  15902  pockthi  16932  matgsum  22380  indistps  22954  indistps2  22955  refun0  23458  filconn  23826  sincosq3sgn  26466  sincosq4sgn  26467  eff1o  26515  ax5seglem7  28919  0grsubgr  29262  nbupgrres  29348  vtxdginducedm1fi  29529  clwwlknclwwlkdif  29965  cnnvg  30664  cnnvs  30666  cnnvnm  30667  h2hva  30960  h2hsm  30961  h2hnm  30962  hhssva  31243  hhsssm  31244  hhssnm  31245  spansnji  31632  lnopunilem1  31996  lnophmlem2  32003  stadd3i  32234  indifundif  32510  dpmul4  32893  xrsp0  33009  xrsp1  33010  hgt750lemd  34685  hgt750lem  34688  rankeq1o  36194  poimirlem8  37657  mbfposadd  37696  iocunico  43210  corcltrcl  43738  binomcxplemdvsum  44354  cosnegpi  45876  fourierdlem62  46177  fouriersw  46240  salexct3  46351  salgensscntex  46353  caragenuncllem  46521  isomenndlem  46539  usgrexmpl2edg  48013