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

Theorem 8p1e9 10111
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 10067 . 2  |-  9  =  ( 8  +  1 )
21eqcomi 2442 1  |-  ( 8  +  1 )  =  9
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083   1c1 8993    + caddc 8995   8c8 10057   9c9 10058
This theorem is referenced by:  cos2bnd  12791  19prm  13442  139prm  13448  317prm  13450  1259lem2  13453  1259lem4  13455  1259lem5  13456  1259prm  13457  2503lem1  13458  2503lem2  13459  2503lem3  13460  4001lem1  13462  quartlem1  20699  log2ub  20791
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-9 10067
  Copyright terms: Public domain W3C validator