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

Theorem 8p1e9 10707
Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
8p1e9  |-  ( 8  +  1 )  =  9

Proof of Theorem 8p1e9
StepHypRef Expression
1 df-9 10642 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2415 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405  (class class class)co 6278   1c1 9523    + caddc 9525   8c8 10632   9c9 10633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-9 10642
This theorem is referenced by:  cos2bnd  14132  19prm  14812  139prm  14818  317prm  14820  1259lem2  14823  1259lem4  14825  1259lem5  14826  1259prm  14827  2503lem1  14828  2503lem2  14829  2503lem3  14830  4001lem1  14832  quartlem1  23513  log2ub  23605  evengpop3  37846  bgoldbtbndlem1  37853
  Copyright terms: Public domain W3C validator