Theorem 8p1e9 12216

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

Syntax hints:   = wceq 1540  (class class class)co 7329  1c1 10965   + caddc 10967  8c8 12127  9c9 12128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728  df-9 12136

This theorem is referenced by:  cos2bnd  15988  19prm  16908  139prm  16914  317prm  16916  1259lem2  16922  1259lem4  16924  1259lem5  16925  1259prm  16926  2503lem1  16927  2503lem2  16928  2503lem3  16929  4001lem1  16931  quartlem1  26105  log2ub  26197  hgt750lem2  32845  lcmineqlem  40307  3lexlogpow5ineq2  40310  aks4d1p1  40331  3cubeslem3l  40758  3cubeslem3r  40759  fmtno5lem3  45347  fmtno5lem4  45348  fmtno4prmfac  45364  fmtno5fac  45374  139prmALT  45388  nfermltl8rev  45534  evengpop3  45590  bgoldbtbndlem1  45597