Theorem 5p1e6 10670

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

Syntax hints:   = wceq 1383  (class class class)co 6281   1c1 9496   + caddc 9498   5c5 10595   6c6 10596

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

This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-6 10605

This theorem is referenced by:  8t8e64  11080  9t7e63  11086  s6len  12841  2exp6OLD  14555  163prm  14592  631prm  14594  1259lem1  14595  1259lem3  14597  1259lem4  14598  2503lem1  14601  2503lem2  14602  4001lem1  14605  4001lem4  14608  4001prm  14609  log2ublem3  23257  log2ub  23258  fib6  28323  5recm6rec  29092