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

Theorem 7p1e8 11589
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 11502 . 2 8 = (7 + 1)
21eqcomi 2781 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1507  (class class class)co 6970  1c1 10328   + caddc 10330  7c7 11493  8c8 11494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-8 11502
This theorem is referenced by:  7t4e28  12017  9t9e81  12035  s8len  14117  prmlem2  16299  83prm  16302  163prm  16304  317prm  16305  631prm  16306  2503lem2  16317  2503lem3  16318  4001lem2  16321  4001lem3  16322  4001prm  16324  hgt750lem  31531  hgt750lem2  31532  fmtno5lem4  43026  fmtno4nprmfac193  43044  m3prm  43062  m7prm  43072  nnsum3primesle9  43267  bgoldbtbndlem1  43278
  Copyright terms: Public domain W3C validator