MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  7p1e8 Structured version   Visualization version   GIF version

Theorem 7p1e8 11778
Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
7p1e8 (7 + 1) = 8

Proof of Theorem 7p1e8
StepHypRef Expression
1 df-8 11698 . 2 8 = (7 + 1)
21eqcomi 2810 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7139  1c1 10531   + caddc 10533  7c7 11689  8c8 11690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-8 11698
This theorem is referenced by:  7t4e28  12201  9t9e81  12219  s8len  14260  prmlem2  16449  83prm  16452  163prm  16454  317prm  16455  631prm  16456  2503lem2  16467  2503lem3  16468  4001lem2  16471  4001lem3  16472  4001prm  16474  hgt750lem  32036  hgt750lem2  32037  lcmineqlem  39339  3cubeslem3l  39620  3cubeslem3r  39621  resqrtvalex  40338  imsqrtvalex  40339  fmtno5lem4  44066  fmtno4nprmfac193  44084  m3prm  44102  m7prm  44110  nnsum3primesle9  44305  bgoldbtbndlem1  44316
  Copyright terms: Public domain W3C validator