Theorem 8p1e9 12409

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11120   + caddc 11122  8c8 12320  9c9 12321

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 2156  ax-ext 2737

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

This theorem is used by:  cos2bnd  16270  19prm  17204  139prm  17210  317prm  17212  1259lem2  17218  1259lem4  17220  1259lem5  17221  1259prm  17222  2503lem1  17223  2503lem2  17224  2503lem3  17225  4001lem1  17227  quartlem1  27077  log2ub  27169  hgt750lem2  35108  lcmineqlem  42881  3lexlogpow5ineq2  42884  aks4d1p1  42905  1p8e9  43094  4p5e9  43103  sum9cubes  43481  3cubeslem3l  43494  3cubeslem3r  43495  fmtno5lem3  48384  fmtno5lem4  48385  fmtno4prmfac  48401  fmtno5fac  48411  139prmALT  48425  nfermltl8rev  48584  evengpop3  48640  bgoldbtbndlem1  48647