Theorem 6p1e7 12388

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

Syntax hints:   = wceq 1540  (class class class)co 7405  1c1 11130   + caddc 11132  6c6 12299  7c7 12300

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 2707

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

This theorem is referenced by:  9t8e72  12836  s7len  14921  37prm  17140  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem3  17152  1259lem4  17153  1259lem5  17154  2503lem1  17156  2503lem2  17157  2503lem3  17158  2503prm  17159  4001lem1  17160  4001lem4  17163  4001prm  17164  log2ublem3  26910  log2ub  26911  hgt750lemd  34680  hgt750lem2  34684  3exp7  42066  3lexlogpow5ineq1  42067  235t711  42354  ex-decpmul  42355  3cubeslem3l  42709  3cubeslem3r  42710  fmtno2  47564  fmtno3  47565  fmtno4  47566  fmtno5lem4  47570  fmtno5  47571  fmtno4nprmfac193  47588  fmtno5fac  47596  127prm  47613  mod42tp1mod8  47616  2exp340mod341  47747  gbowge7  47777  sbgoldbwt  47791  nnsum3primesle9  47808