Theorem 3eqtrri 2637

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

Syntax hints:   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  dfif5  4052  resindm  5364  difxp1  5478  difxp2  5479  dfdm2  5584  cofunex2g  7024  df1st2  7150  df2nd2  7151  domss2  8004  adderpqlem  9655  dfn2  11182  9p1e10  11372  sq10OLD  12913  sqrtm1  13864  0.999...  14451  0.999...OLD  14452  pockthi  15449  matgsum  20062  indistps  20625  indistps2  20626  refun0  21128  filcon  21497  sincosq3sgn  24056  sincosq4sgn  24057  eff1o  24099  ax5seglem7  25615  clwlknclwlkdifs  26487  cnnvg  26917  cnnvs  26919  cnnvnm  26920  h2hva  27215  h2hsm  27216  h2hnm  27217  hhssva  27498  hhsssm  27499  hhssnm  27500  spansnji  27889  lnopunilem1  28253  lnophmlem2  28260  stadd3i  28491  indifundif  28740  xrsp0  29012  xrsp1  29013  rankeq1o  31448  poimirlem8  32587  mbfposadd  32627  iocunico  36815  corcltrcl  37050  binomcxplemdvsum  37576  cosnegpi  38750  fourierdlem62  39061  fouriersw  39124  salexct3  39236  salgensscntex  39238  caragenuncllem  39402  isomenndlem  39420  0grsubgr  40502  nbupgrres  40592  clwwlknclwwlkdifs  41181