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

Theorem 7p1e8 9852
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 9810 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2287 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   7c7 9800   8c8 9801
This theorem is referenced by:  7t4e28  10208  9t9e81  10226  s8len  11546  prmlem2  13121  83prm  13124  163prm  13126  317prm  13127  631prm  13128  2503lem2  13136  2503lem3  13137  4001lem2  13140  4001lem3  13141  4001prm  13143
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-8 9810
  Copyright terms: Public domain W3C validator