Theorem 6p1e7 12318

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

Syntax hints:   = wceq 1542  (class class class)co 7361  1c1 11033   + caddc 11035  6c6 12234  7c7 12235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-7 12243

This theorem is referenced by:  9t8e72  12766  s7len  14858  37prm  17085  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem4  17108  4001prm  17109  log2ublem3  26928  log2ub  26929  hgt750lemd  34811  hgt750lem2  34815  3exp7  42509  3lexlogpow5ineq1  42510  235t711  42754  ex-decpmul  42755  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