Theorem 8p1e9 12331

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  8c8 12247  9c9 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-9 12256

This theorem is referenced by:  cos2bnd  16156  19prm  17088  139prm  17094  317prm  17096  1259lem2  17102  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  quartlem1  26767  log2ub  26859  hgt750lem2  34643  lcmineqlem  42040  3lexlogpow5ineq2  42043  aks4d1p1  42064  sum9cubes  42660  3cubeslem3l  42674  3cubeslem3r  42675  fmtno5lem3  47556  fmtno5lem4  47557  fmtno4prmfac  47573  fmtno5fac  47583  139prmALT  47597  nfermltl8rev  47743  evengpop3  47799  bgoldbtbndlem1  47806