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

Theorem 7p1e8 10746
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 10681 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2462 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446  (class class class)co 6295   1c1 9545    + caddc 9547   7c7 10671   8c8 10672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-cleq 2446  df-8 10681
This theorem is referenced by:  7t4e28  11142  9t9e81  11160  s8len  13004  prmlem2  15103  83prm  15106  163prm  15108  317prm  15109  631prm  15110  2503lem2  15121  2503lem3  15122  4001lem2  15125  4001lem3  15126  4001prm  15128  nnsum3primesle9  38899  bgoldbtbndlem1  38910
  Copyright terms: Public domain W3C validator