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

Theorem 8p1e9 9869
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 9827 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2300 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   8c8 9817   9c9 9818
This theorem is referenced by:  cos2bnd  12484  19prm  13135  139prm  13141  317prm  13143  1259lem2  13146  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  4001lem1  13155  quartlem1  20169  log2ub  20261
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-9 9827
  Copyright terms: Public domain W3C validator