Theorem 8p1e9 12399

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

Syntax hints:   = wceq 1539  (class class class)co 7414  1c1 11139   + caddc 11141  8c8 12310  9c9 12311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

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

This theorem is referenced by:  cos2bnd  16207  19prm  17138  139prm  17144  317prm  17146  1259lem2  17152  1259lem4  17154  1259lem5  17155  1259prm  17156  2503lem1  17157  2503lem2  17158  2503lem3  17159  4001lem1  17161  quartlem1  26855  log2ub  26947  hgt750lem2  34608  lcmineqlem  41994  3lexlogpow5ineq2  41997  aks4d1p1  42018  sum9cubes  42627  3cubeslem3l  42642  3cubeslem3r  42643  fmtno5lem3  47488  fmtno5lem4  47489  fmtno4prmfac  47505  fmtno5fac  47515  139prmALT  47529  nfermltl8rev  47675  evengpop3  47731  bgoldbtbndlem1  47738