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

Theorem 8p1e9 11102
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 11030 . 2 9 = (8 + 1)
21eqcomi 2630 1 (8 + 1) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6604  1c1 9881   + caddc 9883  8c8 11020  9c9 11021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-9 11030
This theorem is referenced by:  cos2bnd  14843  19prm  15749  139prm  15755  317prm  15757  1259lem2  15763  1259lem4  15765  1259lem5  15766  1259prm  15767  2503lem1  15768  2503lem2  15769  2503lem3  15770  4001lem1  15772  quartlem1  24484  log2ub  24576  fmtno5lem3  40763  fmtno5lem4  40764  fmtno4prmfac  40780  fmtno5fac  40790  139prmALT  40807  evengpop3  40972  bgoldbtbndlem1  40979
  Copyright terms: Public domain W3C validator