Theorem 8p1e9 12358

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

Syntax hints:   = wceq 1541  (class class class)co 7405  1c1 11107   + caddc 11109  8c8 12269  9c9 12270

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-9 12278

This theorem is referenced by:  cos2bnd  16127  19prm  17047  139prm  17053  317prm  17055  1259lem2  17061  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  quartlem1  26351  log2ub  26443  hgt750lem2  33652  lcmineqlem  40905  3lexlogpow5ineq2  40908  aks4d1p1  40929  3cubeslem3l  41409  3cubeslem3r  41410  fmtno5lem3  46209  fmtno5lem4  46210  fmtno4prmfac  46226  fmtno5fac  46236  139prmALT  46250  nfermltl8rev  46396  evengpop3  46452  bgoldbtbndlem1  46459