Theorem 8p1e9 12443

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  8c8 12354  9c9 12355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-9 12363

This theorem is referenced by:  cos2bnd  16236  19prm  17165  139prm  17171  317prm  17173  1259lem2  17179  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  quartlem1  26918  log2ub  27010  hgt750lem2  34629  lcmineqlem  42009  3lexlogpow5ineq2  42012  aks4d1p1  42033  sum9cubes  42627  3cubeslem3l  42642  3cubeslem3r  42643  fmtno5lem3  47429  fmtno5lem4  47430  fmtno4prmfac  47446  fmtno5fac  47456  139prmALT  47470  nfermltl8rev  47616  evengpop3  47672  bgoldbtbndlem1  47679