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

Theorem 8p1e9 11765
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 11685 . 2 9 = (8 + 1)
21eqcomi 2830 1 (8 + 1) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7130  1c1 10515   + caddc 10517  8c8 11676  9c9 11677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814  df-9 11685
This theorem is referenced by:  cos2bnd  15520  19prm  16430  139prm  16436  317prm  16438  1259lem2  16444  1259lem4  16446  1259lem5  16447  1259prm  16448  2503lem1  16449  2503lem2  16450  2503lem3  16451  4001lem1  16453  quartlem1  25422  log2ub  25514  hgt750lem2  31931  lcmineqlem  39215  3cubeslem3l  39434  3cubeslem3r  39435  fmtno5lem3  43891  fmtno5lem4  43892  fmtno4prmfac  43908  fmtno5fac  43918  139prmALT  43932  nfermltl8rev  44079  evengpop3  44135  bgoldbtbndlem1  44142
  Copyright terms: Public domain W3C validator