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

Theorem 8p1e9 9853
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 9811 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2287 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858   1c1 8738    + caddc 8740   8c8 9801   9c9 9802
This theorem is referenced by:  cos2bnd  12468  19prm  13119  139prm  13125  317prm  13127  1259lem2  13130  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  4001lem1  13139  quartlem1  20153  log2ub  20245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-9 9811
  Copyright terms: Public domain W3C validator