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

Theorem 3eqtrri 2413
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 2408 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2409 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  dfif5  3695  dfdm2  5342  cofunex2g  5900  difxp1  6321  difxp2  6322  df1st2  6373  df2nd2  6374  domss2  7203  adderpqlem  8765  dfn2  10167  sqrm1  12009  0.999...  12586  pockthi  13203  indistps  16999  indistps2  17000  filcon  17837  sincosq3sgn  20276  sincosq4sgn  20277  eff1o  20319  cnnvg  22018  cnnvs  22021  cnnvnm  22022  h2hva  22326  h2hsm  22327  h2hnm  22328  hhssva  22608  hhsssm  22609  hhssnm  22610  spansnji  22997  lnopunilem1  23362  lnophmlem2  23369  stadd3i  23600  ax5seglem7  25589  rankeq1o  25827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2381
  Copyright terms: Public domain W3C validator