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

Theorem 8p1e9 10043
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 9999 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2393 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6022   1c1 8926    + caddc 8928   8c8 9989   9c9 9990
This theorem is referenced by:  cos2bnd  12718  19prm  13369  139prm  13375  317prm  13377  1259lem2  13380  1259lem4  13382  1259lem5  13383  1259prm  13384  2503lem1  13385  2503lem2  13386  2503lem3  13387  4001lem1  13389  quartlem1  20566  log2ub  20658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-cleq 2382  df-9 9999
  Copyright terms: Public domain W3C validator