Theorem 6p1e7 12300

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

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  6c6 12216  7c7 12217

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  9t8e72  12747  s7len  14837  37prm  17060  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem4  17083  4001prm  17084  log2ublem3  26926  log2ub  26927  hgt750lemd  34826  hgt750lem2  34830  3exp7  42423  3lexlogpow5ineq1  42424  235t711  42675  ex-decpmul  42676  3cubeslem3l  43043  3cubeslem3r  43044  fmtno2  47910  fmtno3  47911  fmtno4  47912  fmtno5lem4  47916  fmtno5  47917  fmtno4nprmfac193  47934  fmtno5fac  47942  127prm  47959  mod42tp1mod8  47962  2exp340mod341  48093  gbowge7  48123  sbgoldbwt  48137  nnsum3primesle9  48154