Theorem 6p1e7 11464

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

Syntax hints:   = wceq 1653  (class class class)co 6876  1c1 10223   + caddc 10225  6c6 11368  7c7 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2790  df-7 11377

This theorem is referenced by:  9t8e72  11909  s7len  13984  37prm  16152  163prm  16156  317prm  16157  631prm  16158  1259lem1  16162  1259lem3  16164  1259lem4  16165  1259lem5  16166  2503lem1  16168  2503lem2  16169  2503lem3  16170  2503prm  16171  4001lem1  16172  4001lem4  16175  4001prm  16176  log2ublem3  25024  log2ub  25025  hgt750lemd  31238  hgt750lem2  31242  235t711  37992  ex-decpmul  37993  fmtno2  42232  fmtno3  42233  fmtno4  42234  fmtno5lem4  42238  fmtno5  42239  fmtno4nprmfac193  42256  fmtno5fac  42264  127prm  42285  mod42tp1mod8  42289  gbowge7  42421  sbgoldbwt  42435  nnsum3primesle9  42452