Theorem 8p1e9 12368

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

Syntax hints:   = wceq 1539  (class class class)co 7413  1c1 11115   + caddc 11117  8c8 12279  9c9 12280

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-9 12288

This theorem is referenced by:  cos2bnd  16137  19prm  17057  139prm  17063  317prm  17065  1259lem2  17071  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  quartlem1  26596  log2ub  26688  hgt750lem2  33960  lcmineqlem  41225  3lexlogpow5ineq2  41228  aks4d1p1  41249  sum9cubes  41718  3cubeslem3l  41728  3cubeslem3r  41729  fmtno5lem3  46523  fmtno5lem4  46524  fmtno4prmfac  46540  fmtno5fac  46550  139prmALT  46564  nfermltl8rev  46710  evengpop3  46766  bgoldbtbndlem1  46773