Theorem 5p1e6 10737

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 10672	. 2 |- 6 = ( 5 + 1 )
2	1	eqcomi 2460	1 |- ( 5 + 1 ) = 6

Syntax hints:   = wceq 1444  (class class class)co 6290   1c1 9540   + caddc 9542   5c5 10662   6c6 10663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-6 10672

This theorem is referenced by:  8t8e64  11145  9t7e63  11151  5recm6rec  11158  s6len  12995  2exp6OLD  15059  163prm  15096  631prm  15098  prmo6  15101  1259lem1  15102  1259lem3  15104  1259lem4  15105  2503lem1  15108  2503lem2  15109  4001lem1  15112  4001lem4  15115  4001prm  15116  log2ublem3  23874  log2ub  23875  fib6  29239  gboge7  38864  gbege6  38866  bgoldbwt  38878  nnsum3primesle9  38889