Theorem 8p1e9 12395

Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
8p1e9	⊢ (8 + 1) = 9

Proof of Theorem 8p1e9

Step	Hyp	Ref	Expression
1		df-9 12315	. 2 ⊢ 9 = (8 + 1)
2	1	eqcomi 2745	1 ⊢ (8 + 1) = 9

Syntax hints:   = wceq 1540  (class class class)co 7410  1c1 11135   + caddc 11137  8c8 12306  9c9 12307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-9 12315

This theorem is referenced by:  cos2bnd  16211  19prm  17142  139prm  17148  317prm  17150  1259lem2  17156  1259lem4  17158  1259lem5  17159  1259prm  17160  2503lem1  17161  2503lem2  17162  2503lem3  17163  4001lem1  17165  quartlem1  26824  log2ub  26916  hgt750lem2  34689  lcmineqlem  42070  3lexlogpow5ineq2  42073  aks4d1p1  42094  sum9cubes  42670  3cubeslem3l  42684  3cubeslem3r  42685  fmtno5lem3  47549  fmtno5lem4  47550  fmtno4prmfac  47566  fmtno5fac  47576  139prmALT  47590  nfermltl8rev  47736  evengpop3  47792  bgoldbtbndlem1  47799