Theorem 6p1e7 12412

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

Syntax hints:   = wceq 1537  (class class class)co 7431  1c1 11154   + caddc 11156  6c6 12323  7c7 12324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  9t8e72  12859  s7len  14938  37prm  17155  163prm  17159  317prm  17160  631prm  17161  1259lem1  17165  1259lem3  17167  1259lem4  17168  1259lem5  17169  2503lem1  17171  2503lem2  17172  2503lem3  17173  2503prm  17174  4001lem1  17175  4001lem4  17178  4001prm  17179  log2ublem3  27006  log2ub  27007  hgt750lemd  34642  hgt750lem2  34646  3exp7  42035  3lexlogpow5ineq1  42036  235t711  42318  ex-decpmul  42319  3cubeslem3l  42674  3cubeslem3r  42675  fmtno2  47475  fmtno3  47476  fmtno4  47477  fmtno5lem4  47481  fmtno5  47482  fmtno4nprmfac193  47499  fmtno5fac  47507  127prm  47524  mod42tp1mod8  47527  2exp340mod341  47658  gbowge7  47688  sbgoldbwt  47702  nnsum3primesle9  47719