Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtrri Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 3eqtri.1 . . 3 𝐴 = 𝐵
2 3eqtri.2 . . 3 𝐵 = 𝐶
31, 2eqtri 2632 . 2 𝐴 = 𝐶
4 3eqtri.3 . 2 𝐶 = 𝐷
53, 4eqtr2i 2633 1 𝐷 = 𝐴
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator