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

Theorem 7p1e8 11358
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 11286 . 2 8 = (7 + 1)
21eqcomi 2779 1 (7 + 1) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  (class class class)co 6792  1c1 10138   + caddc 10140  7c7 11276  8c8 11277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-cleq 2763  df-8 11286
This theorem is referenced by:  7t4e28  11850  9t9e81  11870  s8len  13856  prmlem2  16033  83prm  16036  163prm  16038  317prm  16039  631prm  16040  2503lem2  16051  2503lem3  16052  4001lem2  16055  4001lem3  16056  4001prm  16058  hgt750lem  31063  hgt750lem2  31064  fmtno5lem4  41986  fmtno4nprmfac193  42004  m3prm  42024  m7prm  42034  nnsum3primesle9  42200  bgoldbtbndlem1  42211
  Copyright terms: Public domain W3C validator