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

Theorem 8p1e9 11365
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 11292 . 2 9 = (8 + 1)
21eqcomi 2780 1 (8 + 1) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  (class class class)co 6796  1c1 10143   + caddc 10145  8c8 11282  9c9 11283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-9 11292
This theorem is referenced by:  cos2bnd  15124  19prm  16032  139prm  16038  317prm  16040  1259lem2  16046  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  4001lem1  16055  quartlem1  24805  log2ub  24897  hgt750lem2  31070  fmtno5lem3  41990  fmtno5lem4  41991  fmtno4prmfac  42007  fmtno5fac  42017  139prmALT  42034  evengpop3  42209  bgoldbtbndlem1  42216
  Copyright terms: Public domain W3C validator