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

Theorem 7p1e8 12415
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 12335 . 2 8 = (7 + 1)
21eqcomi 2746 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  7c7 12326  8c8 12327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-8 12335
This theorem is referenced by:  7t4e28  12844  9t9e81  12862  s8len  14942  prmlem2  17157  83prm  17160  163prm  17162  317prm  17163  631prm  17164  2503lem2  17175  2503lem3  17176  4001lem2  17179  4001lem3  17180  4001prm  17182  hgt750lem  34666  hgt750lem2  34667  lcmineqlem  42053  3cubeslem3l  42697  3cubeslem3r  42698  resqrtvalex  43658  imsqrtvalex  43659  fmtno5lem4  47543  fmtno4nprmfac193  47561  m3prm  47579  m7prm  47587  nnsum3primesle9  47781  bgoldbtbndlem1  47792
  Copyright terms: Public domain W3C validator