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

Theorem 7p1e8 9868
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 9826 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2300 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   7c7 9816   8c8 9817
This theorem is referenced by:  7t4e28  10224  9t9e81  10242  s8len  11562  prmlem2  13137  83prm  13140  163prm  13142  317prm  13143  631prm  13144  2503lem2  13152  2503lem3  13153  4001lem2  13156  4001lem3  13157  4001prm  13159
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-8 9826
  Copyright terms: Public domain W3C validator