Theorem 8p1e9 10691

Description: 8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
8p1e9

Proof of Theorem 8p1e9

Step	Hyp	Ref	Expression
1		df-9 10626	. 2
2	1	eqcomi 2470	1

Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514  caddc 9516  8c8 10616  9c9 10617

This theorem is referenced by:  cos2bnd  13923  19prm  14603  139prm  14609  317prm  14611  1259lem2  14614  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  4001lem1  14623  quartlem1  23188  log2ub  23280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-9 10626