Theorem 6p1e7 11033

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

Assertion

Ref	Expression
6p1e7	⊢ (6 + 1) = 7

Proof of Theorem 6p1e7

Step	Hyp	Ref	Expression
1		df-7 10961	. 2 ⊢ 7 = (6 + 1)
2	1	eqcomi 2619	1 ⊢ (6 + 1) = 7

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  6c6 10951  7c7 10952

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-7 10961

This theorem is referenced by:  9t8e72  11545  s7len  13497  37prm  15666  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem3  15678  1259lem4  15679  1259lem5  15680  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem4  15689  4001prm  15690  log2ublem3  24475  log2ub  24476  fmtno2  40000  fmtno3  40001  fmtno4  40002  fmtno5lem4  40006  fmtno5  40007  fmtno4nprmfac193  40024  fmtno5fac  40032  127prm  40053  mod42tp1mod8  40057  gboge7  40185  bgoldbwt  40199  nnsum3primesle9  40210