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

Theorem 7p1e8 11117
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 11045 . 2 8 = (7 + 1)
21eqcomi 2630 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6615  1c1 9897   + caddc 9899  7c7 11035  8c8 11036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-8 11045
This theorem is referenced by:  7t4e28  11610  9t9e81  11630  s8len  13600  prmlem2  15770  83prm  15773  163prm  15775  317prm  15776  631prm  15777  2503lem2  15788  2503lem3  15789  4001lem2  15792  4001lem3  15793  4001prm  15795  fmtno5lem4  40797  fmtno4nprmfac193  40815  m3prm  40835  m7prm  40845  nnsum3primesle9  41001  bgoldbtbndlem1  41012
  Copyright terms: Public domain W3C validator