Theorem 6p1e7 12329

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  6c6 12245  7c7 12246

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 2701

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

This theorem is referenced by:  9t8e72  12777  s7len  14868  37prm  17091  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26858  log2ub  26859  hgt750lemd  34639  hgt750lem2  34643  3exp7  42041  3lexlogpow5ineq1  42042  235t711  42293  ex-decpmul  42294  3cubeslem3l  42674  3cubeslem3r  42675  fmtno2  47551  fmtno3  47552  fmtno4  47553  fmtno5lem4  47557  fmtno5  47558  fmtno4nprmfac193  47575  fmtno5fac  47583  127prm  47600  mod42tp1mod8  47603  2exp340mod341  47734  gbowge7  47764  sbgoldbwt  47778  nnsum3primesle9  47795