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

Theorem 3eqtrri 2466
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 2461 . 2  |-  A  =  C
4 3eqtri.3 . 2  |-  C  =  D
53, 4eqtr2i 2462 1  |-  D  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  dfif5  3802  difxp1  5260  difxp2  5261  dfdm2  5366  cofunex2g  6541  df1st2  6658  df2nd2  6659  domss2  7466  adderpqlem  9119  dfn2  10588  sqrm1  12761  0.999...  13337  pockthi  13964  indistps  18574  indistps2  18575  filcon  19415  sincosq3sgn  21921  sincosq4sgn  21922  eff1o  21964  ax5seglem7  23116  cnnvg  24003  cnnvs  24006  cnnvnm  24007  h2hva  24311  h2hsm  24312  h2hnm  24313  hhssva  24595  hhsssm  24596  hhssnm  24597  spansnji  24984  lnopunilem1  25349  lnophmlem2  25356  stadd3i  25587  xrsp0  26075  xrsp1  26076  rankeq1o  28138  mbfposadd  28364  iocunico  29511  clwlknclwlkdifs  30503
  Copyright terms: Public domain W3C validator