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

Theorem 3eqtrri 2308
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 2303 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2304 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  dfif5  3577  dfdm2  5204  cofunex2g  5740  difxp1  6154  difxp2  6155  df1st2  6205  df2nd2  6206  domss2  7020  adderpqlem  8578  dfn2  9978  sqrm1  11761  0.999...  12337  pockthi  12954  indistps  16748  indistps2  16749  filcon  17578  sincosq3sgn  19868  sincosq4sgn  19869  eff1o  19911  cnnvg  21246  cnnvs  21249  cnnvnm  21250  h2hva  21554  h2hsm  21555  h2hnm  21556  hhssva  21836  hhsssm  21837  hhssnm  21838  spansnji  22225  lnopunilem1  22590  stadd3i  22828  ax5seglem7  24563  rankeq1o  24801  dispos  25287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator