Theorem 8p1e9 12302

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 12227	. 2 ⊢ 9 = (8 + 1)
2	1	eqcomi 2746	1 ⊢ (8 + 1) = 9

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  8c8 12218  9c9 12219

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 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-9 12227

This theorem is referenced by:  cos2bnd  16125  19prm  17057  139prm  17063  317prm  17065  1259lem2  17071  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  quartlem1  26838  log2ub  26930  hgt750lem2  34834  lcmineqlem  42426  3lexlogpow5ineq2  42429  aks4d1p1  42450  sum9cubes  43034  3cubeslem3l  43047  3cubeslem3r  43048  fmtno5lem3  47919  fmtno5lem4  47920  fmtno4prmfac  47936  fmtno5fac  47946  139prmALT  47960  nfermltl8rev  48106  evengpop3  48162  bgoldbtbndlem1  48169