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

Theorem 7p1e8 10705
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 10640 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2415 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405  (class class class)co 6277   1c1 9522    + caddc 9524   7c7 10630   8c8 10631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-8 10640
This theorem is referenced by:  7t4e28  11102  9t9e81  11120  s8len  12915  prmlem2  14812  83prm  14815  163prm  14817  317prm  14818  631prm  14819  2503lem2  14827  2503lem3  14828  4001lem2  14831  4001lem3  14832  4001prm  14834  nnsum3primesle9  37823  bgoldbtbndlem1  37834
  Copyright terms: Public domain W3C validator