Theorem 8p1e9 11365

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

Syntax hints:   = wceq 1631  (class class class)co 6796  1c1 10143   + caddc 10145  8c8 11282  9c9 11283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-9 11292

This theorem is referenced by:  cos2bnd  15124  19prm  16032  139prm  16038  317prm  16040  1259lem2  16046  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  4001lem1  16055  quartlem1  24805  log2ub  24897  hgt750lem2  31070  fmtno5lem3  41990  fmtno5lem4  41991  fmtno4prmfac  42007  fmtno5fac  42017  139prmALT  42034  evengpop3  42209  bgoldbtbndlem1  42216