Theorem 8p1e9 12400

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7416  1c1 11111   + caddc 11113  8c8 12311  9c9 12312

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 2738

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

This theorem is used by:  cos2bnd  16254  19prm  17188  139prm  17194  317prm  17196  1259lem2  17202  1259lem4  17204  1259lem5  17205  1259prm  17206  2503lem1  17207  2503lem2  17208  2503lem3  17209  4001lem1  17211  quartlem1  27037  log2ub  27129  hgt750lem2  35052  lcmineqlem  42851  3lexlogpow5ineq2  42854  aks4d1p1  42875  sum9cubes  43436  3cubeslem3l  43449  3cubeslem3r  43450  fmtno5lem3  48339  fmtno5lem4  48340  fmtno4prmfac  48356  fmtno5fac  48366  139prmALT  48380  nfermltl8rev  48539  evengpop3  48595  bgoldbtbndlem1  48602