Theorem 6p1e7 11358

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

Syntax hints:   = wceq 1631  (class class class)co 6793  1c1 10139   + caddc 10141  6c6 11276  7c7 11277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-7 11286

This theorem is referenced by:  9t8e72  11870  s7len  13856  37prm  16035  163prm  16039  317prm  16040  631prm  16041  1259lem1  16045  1259lem3  16047  1259lem4  16048  1259lem5  16049  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem4  16058  4001prm  16059  log2ublem3  24896  log2ub  24897  hgt750lemd  31066  hgt750lem2  31070  fmtno2  41990  fmtno3  41991  fmtno4  41992  fmtno5lem4  41996  fmtno5  41997  fmtno4nprmfac193  42014  fmtno5fac  42022  127prm  42043  mod42tp1mod8  42047  gbowge7  42179  sbgoldbwt  42193  nnsum3primesle9  42210