Theorem 6p1e7 12414

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

Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  6c6 12325  7c7 12326

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  9t8e72  12861  s7len  14941  37prm  17158  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem4  17181  4001prm  17182  log2ublem3  26991  log2ub  26992  hgt750lemd  34663  hgt750lem2  34667  3exp7  42054  3lexlogpow5ineq1  42055  235t711  42339  ex-decpmul  42340  3cubeslem3l  42697  3cubeslem3r  42698  fmtno2  47537  fmtno3  47538  fmtno4  47539  fmtno5lem4  47543  fmtno5  47544  fmtno4nprmfac193  47561  fmtno5fac  47569  127prm  47586  mod42tp1mod8  47589  2exp340mod341  47720  gbowge7  47750  sbgoldbwt  47764  nnsum3primesle9  47781