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 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  dfif5  4483  resindm  5995  difxp1  6129  difxp2  6130  dfdm2  6245  cofunex2g  7903  df1st2  8048  df2nd2  8049  domss2  9074  adderpqlem  10877  dfn2  12450  9p1e10  12646  sqrtm1  15237  0.999...  15846  pockthi  16878  matgsum  22402  indistps  22976  indistps2  22977  refun0  23480  filconn  23848  sincosq3sgn  26464  sincosq4sgn  26465  eff1o  26513  ax5seglem7  29004  0grsubgr  29347  nbupgrres  29433  vtxdginducedm1fi  29613  clwwlknclwwlkdif  30049  cnnvg  30749  cnnvs  30751  cnnvnm  30752  h2hva  31045  h2hsm  31046  h2hnm  31047  hhssva  31328  hhsssm  31329  hhssnm  31330  spansnji  31717  lnopunilem1  32081  lnophmlem2  32088  stadd3i  32319  indifundif  32594  dpmul4  32973  xrsp0  33072  xrsp1  33073  hgt750lemd  34792  hgt750lem  34795  rankeq1o  36353  poimirlem8  37949  mbfposadd  37988  iocunico  43639  corcltrcl  44166  binomcxplemdvsum  44782  cosnegpi  46295  fourierdlem62  46596  fouriersw  46659  salexct3  46770  salgensscntex  46772  caragenuncllem  46940  isomenndlem  46958  goldratmolem2  47334  usgrexmpl2edg  48505