Theorem 6p1e7 12305

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  6c6 12221  7c7 12222

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 12230

This theorem is referenced by:  9t8e72  12753  s7len  14844  37prm  17067  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem4  17090  4001prm  17091  log2ublem3  26834  log2ub  26835  hgt750lemd  34612  hgt750lem2  34616  3exp7  42014  3lexlogpow5ineq1  42015  235t711  42266  ex-decpmul  42267  3cubeslem3l  42647  3cubeslem3r  42648  fmtno2  47524  fmtno3  47525  fmtno4  47526  fmtno5lem4  47530  fmtno5  47531  fmtno4nprmfac193  47548  fmtno5fac  47556  127prm  47573  mod42tp1mod8  47576  2exp340mod341  47707  gbowge7  47737  sbgoldbwt  47751  nnsum3primesle9  47768