Theorem 8p1e9 12416

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

Syntax hints:   = wceq 1534  (class class class)co 7426  1c1 11161   + caddc 11163  8c8 12327  9c9 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-9 12336

This theorem is referenced by:  cos2bnd  16192  19prm  17122  139prm  17128  317prm  17130  1259lem2  17136  1259lem4  17138  1259lem5  17139  1259prm  17140  2503lem1  17141  2503lem2  17142  2503lem3  17143  4001lem1  17145  quartlem1  26888  log2ub  26980  hgt750lem2  34500  lcmineqlem  41753  3lexlogpow5ineq2  41756  aks4d1p1  41777  sum9cubes  42344  3cubeslem3l  42361  3cubeslem3r  42362  fmtno5lem3  47145  fmtno5lem4  47146  fmtno4prmfac  47162  fmtno5fac  47172  139prmALT  47186  nfermltl8rev  47332  evengpop3  47388  bgoldbtbndlem1  47395