Theorem 8p1e9 12318

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

Syntax hints:   = wceq 1547  (class class class)co 7357  1c1 11031   + caddc 11033  8c8 12234  9c9 12235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-9 12243

This theorem is referenced by:  cos2bnd  16147  19prm  17080  139prm  17086  317prm  17088  1259lem2  17094  1259lem4  17096  1259lem5  17097  1259prm  17098  2503lem1  17099  2503lem2  17100  2503lem3  17101  4001lem1  17103  quartlem1  26840  log2ub  26932  hgt750lem2  34845  lcmineqlem  42546  3lexlogpow5ineq2  42549  aks4d1p1  42570  sum9cubes  43131  3cubeslem3l  43144  3cubeslem3r  43145  fmtno5lem3  48041  fmtno5lem4  48042  fmtno4prmfac  48058  fmtno5fac  48068  139prmALT  48082  nfermltl8rev  48241  evengpop3  48297  bgoldbtbndlem1  48304