Theorem 8p1e9 12288

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  8c8 12204  9c9 12205

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-9 12213

This theorem is referenced by:  cos2bnd  16111  19prm  17043  139prm  17049  317prm  17051  1259lem2  17057  1259lem4  17059  1259lem5  17060  1259prm  17061  2503lem1  17062  2503lem2  17063  2503lem3  17064  4001lem1  17066  quartlem1  26821  log2ub  26913  hgt750lem2  34758  lcmineqlem  42245  3lexlogpow5ineq2  42248  aks4d1p1  42269  sum9cubes  42857  3cubeslem3l  42870  3cubeslem3r  42871  fmtno5lem3  47743  fmtno5lem4  47744  fmtno4prmfac  47760  fmtno5fac  47770  139prmALT  47784  nfermltl8rev  47930  evengpop3  47986  bgoldbtbndlem1  47993