Theorem 8p1e9 12368

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

Syntax hints:   = wceq 1561  (class class class)co 7397  1c1 11075   + caddc 11077  8c8 12279  9c9 12280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-9 12288

This theorem is referenced by:  cos2bnd  16221  19prm  17155  139prm  17161  317prm  17163  1259lem2  17169  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  4001lem1  17178  quartlem1  26923  log2ub  27015  hgt750lem2  34947  lcmineqlem  42670  3lexlogpow5ineq2  42673  aks4d1p1  42694  sum9cubes  43255  3cubeslem3l  43268  3cubeslem3r  43269  fmtno5lem3  48165  fmtno5lem4  48166  fmtno4prmfac  48182  fmtno5fac  48192  139prmALT  48206  nfermltl8rev  48365  evengpop3  48421  bgoldbtbndlem1  48428