Theorem 8p1e9 12436

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7415  1c1 11147   + caddc 11149  8c8 12347  9c9 12348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-9 12356

This theorem is used by:  cos2bnd  16298  19prm  17232  139prm  17238  317prm  17240  1259lem2  17246  1259lem4  17248  1259lem5  17249  1259prm  17250  2503lem1  17251  2503lem2  17252  2503lem3  17253  4001lem1  17255  quartlem1  27123  log2ub  27215  hgt750lem2  35190  lcmineqlem  42932  3lexlogpow5ineq2  42935  aks4d1p1  42956  1p8e9  43145  4p5e9  43154  sum9cubes  43532  3cubeslem3l  43545  3cubeslem3r  43546  fmtno5lem3  48472  fmtno5lem4  48473  fmtno4prmfac  48489  fmtno5fac  48499  139prmALT  48513  nfermltl8rev  48672  evengpop3  48728  bgoldbtbndlem1  48735