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

Theorem 7p1e8 12236
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 12156 . 2 8 = (7 + 1)
21eqcomi 2747 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  1c1 10986   + caddc 10988  7c7 12147  8c8 12148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-8 12156
This theorem is referenced by:  7t4e28  12663  9t9e81  12681  s8len  14725  prmlem2  16928  83prm  16931  163prm  16933  317prm  16934  631prm  16935  2503lem2  16946  2503lem3  16947  4001lem2  16950  4001lem3  16951  4001prm  16953  hgt750lem  33044  hgt750lem2  33045  lcmineqlem  40440  3cubeslem3l  40911  3cubeslem3r  40912  resqrtvalex  41716  imsqrtvalex  41717  fmtno5lem4  45539  fmtno4nprmfac193  45557  m3prm  45575  m7prm  45583  nnsum3primesle9  45777  bgoldbtbndlem1  45788
  Copyright terms: Public domain W3C validator