MPE Home 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  |-  A  =  B
3eqtri.2  |-  B  =  C
3eqtri.3  |-  C  =  D
Assertion
Ref Expression
3eqtrri  |-  D  =  A

Proof of Theorem 3eqtrri
StepHypRef Expression
1 3eqtri.1 . . 3  |-  A  =  B
2 3eqtri.2 . . 3  |-  B  =  C
31, 2eqtri 2496 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2497 1  |-  D  =  A
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