Theorem 5p1e6 10738

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

Assertion

Ref	Expression
5p1e6	|- ( 5 + 1 ) = 6

Proof of Theorem 5p1e6

Step	Hyp	Ref	Expression
1		df-6 10673	. 2 |- 6 = ( 5 + 1 )
2	1	eqcomi 2435	1 |- ( 5 + 1 ) = 6

Syntax hints:   = wceq 1437  (class class class)co 6302   1c1 9541   + caddc 9543   5c5 10663   6c6 10664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-6 10673

This theorem is referenced by:  8t8e64  11146  9t7e63  11152  5recm6rec  11159  s6len  12985  2exp6OLD  15047  163prm  15084  631prm  15086  prmo6  15089  1259lem1  15090  1259lem3  15092  1259lem4  15093  2503lem1  15096  2503lem2  15097  4001lem1  15100  4001lem4  15103  4001prm  15104  log2ublem3  23861  log2ub  23862  fib6  29235  gboge7  38576  gbege6  38578  bgoldbwt  38590  nnsum3primesle9  38601