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

Theorem 7p1e8 10108
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 10064 . 2  |-  8  =  ( 7  +  1 )
21eqcomi 2440 1  |-  ( 7  +  1 )  =  8
Colors of variables: wff set class
Syntax hints:    = wceq 1652  (class class class)co 6081   1c1 8991    + caddc 8993   7c7 10054   8c8 10055
This theorem is referenced by:  7t4e28  10466  9t9e81  10484  s8len  11860  prmlem2  13442  83prm  13445  163prm  13447  317prm  13448  631prm  13449  2503lem2  13457  2503lem3  13458  4001lem2  13461  4001lem3  13462  4001prm  13464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429  df-8 10064
  Copyright terms: Public domain W3C validator