Theorem 6p1e7 12271

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  6c6 12187  7c7 12188

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  9t8e72  12719  s7len  14809  37prm  17032  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem4  17055  4001prm  17056  log2ublem3  26856  log2ub  26857  hgt750lemd  34616  hgt750lem2  34620  3exp7  42026  3lexlogpow5ineq1  42027  235t711  42278  ex-decpmul  42279  3cubeslem3l  42659  3cubeslem3r  42660  fmtno2  47534  fmtno3  47535  fmtno4  47536  fmtno5lem4  47540  fmtno5  47541  fmtno4nprmfac193  47558  fmtno5fac  47566  127prm  47583  mod42tp1mod8  47586  2exp340mod341  47717  gbowge7  47747  sbgoldbwt  47761  nnsum3primesle9  47778