Theorem 6p1e7 12315

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

Syntax hints:   = wceq 1547  (class class class)co 7356  1c1 11030   + caddc 11032  6c6 12231  7c7 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-7 12240

This theorem is referenced by:  9t8e72  12763  s7len  14855  37prm  17082  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem4  17105  4001prm  17106  log2ublem3  26930  log2ub  26931  hgt750lemd  34832  hgt750lem2  34836  3exp7  42538  3lexlogpow5ineq1  42539  235t711  42782  ex-decpmul  42783  3cubeslem3l  43135  3cubeslem3r  43136  fmtno2  48028  fmtno3  48029  fmtno4  48030  fmtno5lem4  48034  fmtno5  48035  fmtno4nprmfac193  48052  fmtno5fac  48060  127prm  48077  mod42tp1mod8  48080  ppivalnn4  48105  2exp340mod341  48224  gbowge7  48254  sbgoldbwt  48268  nnsum3primesle9  48285