Theorem 6p1e7 11156

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 11084	. 2 ⊢ 7 = (6 + 1)
2	1	eqcomi 2631	1 ⊢ (6 + 1) = 7

Syntax hints:   = wceq 1483  (class class class)co 6650  1c1 9937   + caddc 9939  6c6 11074  7c7 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-7 11084

This theorem is referenced by:  9t8e72  11669  s7len  13647  37prm  15828  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem3  15840  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem4  15851  4001prm  15852  log2ublem3  24675  log2ub  24676  hgt750lemd  30726  hgt750lem2  30730  fmtno2  41462  fmtno3  41463  fmtno4  41464  fmtno5lem4  41468  fmtno5  41469  fmtno4nprmfac193  41486  fmtno5fac  41494  127prm  41515  mod42tp1mod8  41519  gbowge7  41651  sbgoldbwt  41665  nnsum3primesle9  41682