Theorem 6p1e7 12497

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424  1c1 11208   + caddc 11210  6c6 12408  7c7 12409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-7 12417

This theorem is used by:  9t8e72  12954  s7len  15062  37prm  17308  163prm  17312  317prm  17313  631prm  17314  1259lem1  17318  1259lem3  17320  1259lem4  17321  1259lem5  17322  2503lem1  17324  2503lem2  17325  2503lem3  17326  2503prm  17327  4001lem1  17328  4001lem4  17331  4001prm  17332  log2ublem3  27285  log2ub  27286  hgt750lemd  35327  hgt750lem2  35331  3exp7  43212  3lexlogpow5ineq1  43213  25or6to4  43365  1p6e7  43422  235t711  43471  ex-decpmul  43472  3cubeslem3l  43805  3cubeslem3r  43806  fmtno2  48743  fmtno3  48744  fmtno4  48745  fmtno5lem4  48749  fmtno5  48750  fmtno4nprmfac193  48767  fmtno5fac  48775  127prm  48792  mod42tp1mod8  48795  ppivalnn4  48820  2exp340mod341  48939  gbowge7  48969  sbgoldbwt  48983  nnsum3primesle9  49000