Theorem 3eqtrri 2790

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

Syntax hints:   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  dfif5  4497  resindmOLD  6017  difxp1  6150  difxp2  6151  dfdm2  6268  cofunex2g  7931  df1st2  8077  df2nd2  8078  domss2  9108  adderpqlem  10912  dfn2  12494  9p1e10  12690  sqrtm1  15302  0.999...  15911  pockthi  16943  matgsum  22494  indistps  23068  indistps2  23069  refun0  23572  filconn  23940  sincosq3sgn  26562  sincosq4sgn  26563  eff1o  26611  ax5seglem7  29133  0grsubgr  29476  nbupgrres  29562  vtxdginducedm1fi  29742  clwwlknclwwlkdif  30178  cnnvg  30878  cnnvs  30880  cnnvnm  30881  h2hva  31174  h2hsm  31175  h2hnm  31176  hhssva  31457  hhsssm  31458  hhssnm  31459  spansnji  31846  lnopunilem1  32210  lnophmlem2  32217  stadd3i  32448  indifundif  32720  dpmul4  33088  xrsp0  33187  xrsp1  33188  hgt750lemd  34939  hgt750lem  34942  rankeq1o  36518  poimirlem8  38124  mbfposadd  38163  iocunico  43785  corcltrcl  44312  binomcxplemdvsum  44928  cosnegpi  46438  fourierdlem62  46739  fouriersw  46802  salexct3  46913  salgensscntex  46915  caragenuncllem  47083  isomenndlem  47101  goldratmolem2  47477  usgrexmpl2edg  48648