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

Theorem 3eqtrri 2460
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 2455 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2456 1  |-  D  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  dfif5  3743  dfdm2  5393  cofunex2g  5952  difxp1  6373  difxp2  6374  df1st2  6425  df2nd2  6426  domss2  7258  adderpqlem  8823  dfn2  10226  sqrm1  12073  0.999...  12650  pockthi  13267  indistps  17067  indistps2  17068  filcon  17907  sincosq3sgn  20400  sincosq4sgn  20401  eff1o  20443  cnnvg  22161  cnnvs  22164  cnnvnm  22165  h2hva  22469  h2hsm  22470  h2hnm  22471  hhssva  22751  hhsssm  22752  hhssnm  22753  spansnji  23140  lnopunilem1  23505  lnophmlem2  23512  stadd3i  23743  xrsp0  24195  xrsp1  24196  ax5seglem7  25866  rankeq1o  26104  mbfposadd  26244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator