Theorem 6p1e7 11788

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

Syntax hints:   = wceq 1537  (class class class)co 7158  1c1 10540   + caddc 10542  6c6 11699  7c7 11700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-7 11708

This theorem is referenced by:  9t8e72  12229  s7len  14266  37prm  16456  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem4  16479  4001prm  16480  log2ublem3  25528  log2ub  25529  hgt750lemd  31921  hgt750lem2  31925  235t711  39184  ex-decpmul  39185  3cubeslem3l  39290  3cubeslem3r  39291  fmtno2  43719  fmtno3  43720  fmtno4  43721  fmtno5lem4  43725  fmtno5  43726  fmtno4nprmfac193  43743  fmtno5fac  43751  127prm  43770  mod42tp1mod8  43774  2exp340mod341  43905  gbowge7  43935  sbgoldbwt  43949  nnsum3primesle9  43966