Theorem 6p1e7 12360

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

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113  6c6 12271  7c7 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-7 12280

This theorem is referenced by:  9t8e72  12805  s7len  14853  37prm  17054  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem4  17077  4001prm  17078  log2ublem3  26453  log2ub  26454  hgt750lemd  33660  hgt750lem2  33664  3exp7  40918  3lexlogpow5ineq1  40919  235t711  41205  ex-decpmul  41206  3cubeslem3l  41424  3cubeslem3r  41425  fmtno2  46218  fmtno3  46219  fmtno4  46220  fmtno5lem4  46224  fmtno5  46225  fmtno4nprmfac193  46242  fmtno5fac  46250  127prm  46267  mod42tp1mod8  46270  2exp340mod341  46401  gbowge7  46431  sbgoldbwt  46445  nnsum3primesle9  46462