Theorem 8p1e9 12292

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11029   + caddc 11031  8c8 12208  9c9 12209

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 2708

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

This theorem is referenced by:  cos2bnd  16115  19prm  17047  139prm  17053  317prm  17055  1259lem2  17061  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  quartlem1  26825  log2ub  26917  hgt750lem2  34811  lcmineqlem  42328  3lexlogpow5ineq2  42331  aks4d1p1  42352  sum9cubes  42936  3cubeslem3l  42949  3cubeslem3r  42950  fmtno5lem3  47822  fmtno5lem4  47823  fmtno4prmfac  47839  fmtno5fac  47849  139prmALT  47863  nfermltl8rev  48009  evengpop3  48065  bgoldbtbndlem1  48072