Theorem 8p1e9 11035

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

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  8c8 10953  9c9 10954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-9 10963

This theorem is referenced by:  cos2bnd  14757  19prm  15663  139prm  15669  317prm  15671  1259lem2  15677  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  4001lem1  15686  quartlem1  24384  log2ub  24476  fmtno5lem3  40005  fmtno5lem4  40006  fmtno4prmfac  40022  fmtno5fac  40032  139prmALT  40049  evengpop3  40214  bgoldbtbndlem1  40221