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

Theorem 3eqtrri 2501
 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 2496 . 2
4 3eqtri.3 . 2
53, 4eqtr2i 2497 1
 Colors of variables: wff setvar class Syntax hints:   wceq 1379 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-cleq 2459 This theorem is referenced by:  dfif5  3955  difxp1  5430  difxp2  5431  dfdm2  5537  cofunex2g  6746  df1st2  6866  df2nd2  6867  domss2  7673  adderpqlem  9328  dfn2  10804  sqrtm1  13068  0.999...  13649  pockthi  14280  matgsum  18706  indistps  19278  indistps2  19279  filcon  20119  sincosq3sgn  22626  sincosq4sgn  22627  eff1o  22669  ax5seglem7  23914  clwlknclwlkdifs  24636  cnnvg  25259  cnnvs  25262  cnnvnm  25263  h2hva  25567  h2hsm  25568  h2hnm  25569  hhssva  25851  hhsssm  25852  hhssnm  25853  spansnji  26240  lnopunilem1  26605  lnophmlem2  26612  stadd3i  26843  xrsp0  27331  xrsp1  27332  rankeq1o  29405  mbfposadd  29639  iocunico  30783  cosnegpi  31203  fourierdlem57  31464  fourierdlem62  31469  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem102  31509  fourierdlem112  31519  fourierdlem114  31521  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532
 Copyright terms: Public domain W3C validator