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

Theorem 7p1e8 10741
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 10676 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2436 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438  (class class class)co 6303   1c1 9542    + caddc 9544   7c7 10666   8c8 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-cleq 2415  df-8 10676
This theorem is referenced by:  7t4e28  11137  9t9e81  11155  s8len  12992  prmlem2  15084  83prm  15087  163prm  15089  317prm  15090  631prm  15091  2503lem2  15102  2503lem3  15103  4001lem2  15106  4001lem3  15107  4001prm  15109  nnsum3primesle9  38645  bgoldbtbndlem1  38656
  Copyright terms: Public domain W3C validator