Theorem 6p1e7 12336

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  6c6 12252  7c7 12253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-7 12261

This theorem is referenced by:  9t8e72  12784  s7len  14875  37prm  17098  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem4  17121  4001prm  17122  log2ublem3  26865  log2ub  26866  hgt750lemd  34646  hgt750lem2  34650  3exp7  42048  3lexlogpow5ineq1  42049  235t711  42300  ex-decpmul  42301  3cubeslem3l  42681  3cubeslem3r  42682  fmtno2  47555  fmtno3  47556  fmtno4  47557  fmtno5lem4  47561  fmtno5  47562  fmtno4nprmfac193  47579  fmtno5fac  47587  127prm  47604  mod42tp1mod8  47607  2exp340mod341  47738  gbowge7  47768  sbgoldbwt  47782  nnsum3primesle9  47799