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

Theorem 8p1e9 11350
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 11278 . 2 9 = (8 + 1)
21eqcomi 2769 1 (8 + 1) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6813  1c1 10129   + caddc 10131  8c8 11268  9c9 11269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-9 11278
This theorem is referenced by:  cos2bnd  15117  19prm  16027  139prm  16033  317prm  16035  1259lem2  16041  1259lem4  16043  1259lem5  16044  1259prm  16045  2503lem1  16046  2503lem2  16047  2503lem3  16048  4001lem1  16050  quartlem1  24783  log2ub  24875  hgt750lem2  31039  fmtno5lem3  41977  fmtno5lem4  41978  fmtno4prmfac  41994  fmtno5fac  42004  139prmALT  42021  evengpop3  42196  bgoldbtbndlem1  42203
  Copyright terms: Public domain W3C validator