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  5351  difxp1  5464  difxp2  5465  dfdm2  5570  cofunex2g  7002  df1st2  7128  df2nd2  7129  domss2  7982  adderpqlem  9633  dfn2  11155  9p1e10  11331  sq10OLD  12871  sqrtm1  13813  0.999...  14400  0.999...OLD  14401  pockthi  15398  matgsum  20010  indistps  20573  indistps2  20574  refun0  21076  filcon  21445  sincosq3sgn  24001  sincosq4sgn  24002  eff1o  24044  ax5seglem7  25561  clwlknclwlkdifs  26281  cnnvg  26711  cnnvs  26713  cnnvnm  26714  h2hva  27009  h2hsm  27010  h2hnm  27011  hhssva  27292  hhsssm  27293  hhssnm  27294  spansnji  27683  lnopunilem1  28047  lnophmlem2  28054  stadd3i  28285  indifundif  28534  xrsp0  28806  xrsp1  28807  rankeq1o  31242  poimirlem8  32381  mbfposadd  32421  iocunico  36609  corcltrcl  36844  binomcxplemdvsum  37370  cosnegpi  38544  fourierdlem62  38855  fouriersw  38918  salexct3  39030  salgensscntex  39032  caragenuncllem  39196  isomenndlem  39214  0grsubgr  40494  nbupgrres  40584  clwwlknclwwlkdifs  41173