Theorem 6p1e7 11773

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  6c6 11684  7c7 11685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-7 11693

This theorem is referenced by:  9t8e72  12214  s7len  14255  37prm  16446  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem4  16469  4001prm  16470  log2ublem3  25534  log2ub  25535  hgt750lemd  32029  hgt750lem2  32033  235t711  39485  ex-decpmul  39486  3cubeslem3l  39627  3cubeslem3r  39628  fmtno2  44067  fmtno3  44068  fmtno4  44069  fmtno5lem4  44073  fmtno5  44074  fmtno4nprmfac193  44091  fmtno5fac  44099  127prm  44116  mod42tp1mod8  44120  2exp340mod341  44251  gbowge7  44281  sbgoldbwt  44295  nnsum3primesle9  44312