Theorem 5p1e6 11032

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 10960	. 2 ⊢ 6 = (5 + 1)
2	1	eqcomi 2619	1 ⊢ (5 + 1) = 6

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  5c5 10950  6c6 10951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-6 10960

This theorem is referenced by:  8t8e64  11538  9t7e63  11544  5recm6rec  11562  fldiv4p1lem1div2  12498  s6len  13496  163prm  15670  631prm  15672  prmo6  15675  1259lem1  15676  1259lem4  15679  2503lem1  15682  2503lem2  15683  4001lem1  15686  4001lem4  15689  4001prm  15690  log2ublem3  24475  log2ub  24476  fib6  29795  fmtno5lem2  40004  fmtno5lem3  40005  fmtno5lem4  40006  fmtno4prmfac193  40023  fmtno4nprmfac193  40024  fmtno5faclem3  40031  flsqrt5  40047  127prm  40053  gboge7  40185  gbege6  40187  bgoldbwt  40199  nnsum3primesle9  40210