Theorem 5p1e6 10663

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

Syntax hints:   = wceq 1379  (class class class)co 6284   1c1 9493   + caddc 9495   5c5 10588   6c6 10589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-6 10598

This theorem is referenced by:  8t8e64  11070  9t7e63  11076  s6len  12822  2exp6  14431  163prm  14468  631prm  14470  1259lem1  14471  1259lem3  14473  1259lem4  14474  2503lem1  14477  2503lem2  14478  4001lem1  14481  4001lem4  14484  4001prm  14485  log2ublem3  23035  log2ub  23036  fib6  28013  5recm6rec  28617