Theorem 8p1e9 11809

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

Syntax hints:   = wceq 1539  (class class class)co 7143  1c1 10561   + caddc 10563  8c8 11720  9c9 11721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-9 11729

This theorem is referenced by:  cos2bnd  15574  19prm  16494  139prm  16500  317prm  16502  1259lem2  16508  1259lem4  16510  1259lem5  16511  1259prm  16512  2503lem1  16513  2503lem2  16514  2503lem3  16515  4001lem1  16517  quartlem1  25527  log2ub  25619  hgt750lem2  32136  lcmineqlem  39604  3lexlogpow5ineq2  39607  aks4d1p1  39627  3cubeslem3l  39985  3cubeslem3r  39986  fmtno5lem3  44425  fmtno5lem4  44426  fmtno4prmfac  44442  fmtno5fac  44452  139prmALT  44466  nfermltl8rev  44612  evengpop3  44668  bgoldbtbndlem1  44675