Theorem 8p1e9 12414

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

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  8c8 12325  9c9 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-9 12334

This theorem is referenced by:  cos2bnd  16221  19prm  17152  139prm  17158  317prm  17160  1259lem2  17166  1259lem4  17168  1259lem5  17169  1259prm  17170  2503lem1  17171  2503lem2  17172  2503lem3  17173  4001lem1  17175  quartlem1  26915  log2ub  27007  hgt750lem2  34646  lcmineqlem  42034  3lexlogpow5ineq2  42037  aks4d1p1  42058  sum9cubes  42659  3cubeslem3l  42674  3cubeslem3r  42675  fmtno5lem3  47480  fmtno5lem4  47481  fmtno4prmfac  47497  fmtno5fac  47507  139prmALT  47521  nfermltl8rev  47667  evengpop3  47723  bgoldbtbndlem1  47730