Theorem 6p1e7 12412

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413  1c1 11125   + caddc 11127  6c6 12323  7c7 12324

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-7 12332

This theorem is used by:  9t8e72  12869  s7len  14973  37prm  17213  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem3  17225  1259lem4  17226  1259lem5  17227  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem4  17236  4001prm  17237  log2ublem3  27185  log2ub  27186  hgt750lemd  35156  hgt750lem2  35160  3exp7  42919  3lexlogpow5ineq1  42920  25or6to4  43072  1p6e7  43129  235t711  43180  ex-decpmul  43181  3cubeslem3l  43531  3cubeslem3r  43532  fmtno2  48453  fmtno3  48454  fmtno4  48455  fmtno5lem4  48459  fmtno5  48460  fmtno4nprmfac193  48477  fmtno5fac  48485  127prm  48502  mod42tp1mod8  48505  ppivalnn4  48530  2exp340mod341  48649  gbowge7  48679  sbgoldbwt  48693  nnsum3primesle9  48710