Theorem 8p1e9 11775

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  8c8 11686  9c9 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-9 11695

This theorem is referenced by:  cos2bnd  15533  19prm  16443  139prm  16449  317prm  16451  1259lem2  16457  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  4001lem1  16466  quartlem1  25443  log2ub  25535  hgt750lem2  32033  lcmineqlem  39340  3cubeslem3l  39627  3cubeslem3r  39628  fmtno5lem3  44072  fmtno5lem4  44073  fmtno4prmfac  44089  fmtno5fac  44099  139prmALT  44113  nfermltl8rev  44260  evengpop3  44316  bgoldbtbndlem1  44323