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

Theorem 8p1e9 10101
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 10057 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2439 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1652  (class class class)co 6073   1c1 8983    + caddc 8985   8c8 10047   9c9 10048
This theorem is referenced by:  cos2bnd  12781  19prm  13432  139prm  13438  317prm  13440  1259lem2  13443  1259lem4  13445  1259lem5  13446  1259prm  13447  2503lem1  13448  2503lem2  13449  2503lem3  13450  4001lem1  13452  quartlem1  20689  log2ub  20781
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 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428  df-9 10057
  Copyright terms: Public domain W3C validator