Theorem 6p1e7 12286

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  6c6 12202  7c7 12203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-7 12211

This theorem is referenced by:  9t8e72  12733  s7len  14823  37prm  17046  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem4  17069  4001prm  17070  log2ublem3  26912  log2ub  26913  hgt750lemd  34754  hgt750lem2  34758  3exp7  42246  3lexlogpow5ineq1  42247  235t711  42502  ex-decpmul  42503  3cubeslem3l  42870  3cubeslem3r  42871  fmtno2  47738  fmtno3  47739  fmtno4  47740  fmtno5lem4  47744  fmtno5  47745  fmtno4nprmfac193  47762  fmtno5fac  47770  127prm  47787  mod42tp1mod8  47790  2exp340mod341  47921  gbowge7  47951  sbgoldbwt  47965  nnsum3primesle9  47982