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

Theorem 8p1e9 12310
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 12230 . 2 9 = (8 + 1)
21eqcomi 2746 1 (8 + 1) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7362  1c1 11059   + caddc 11061  8c8 12221  9c9 12222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-9 12230
This theorem is referenced by:  cos2bnd  16077  19prm  16997  139prm  17003  317prm  17005  1259lem2  17011  1259lem4  17013  1259lem5  17014  1259prm  17015  2503lem1  17016  2503lem2  17017  2503lem3  17018  4001lem1  17020  quartlem1  26223  log2ub  26315  hgt750lem2  33305  lcmineqlem  40538  3lexlogpow5ineq2  40541  aks4d1p1  40562  3cubeslem3l  41038  3cubeslem3r  41039  fmtno5lem3  45821  fmtno5lem4  45822  fmtno4prmfac  45838  fmtno5fac  45848  139prmALT  45862  nfermltl8rev  46008  evengpop3  46064  bgoldbtbndlem1  46071
  Copyright terms: Public domain W3C validator