Theorem 6p1e7 12403

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11116   + caddc 11118  6c6 12314  7c7 12315

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 2156  ax-ext 2737

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

This theorem is used by:  9t8e72  12860  s7len  14963  37prm  17203  163prm  17207  317prm  17208  631prm  17209  1259lem1  17213  1259lem3  17215  1259lem4  17216  1259lem5  17217  2503lem1  17219  2503lem2  17220  2503lem3  17221  2503prm  17222  4001lem1  17223  4001lem4  17226  4001prm  17227  log2ublem3  27164  log2ub  27165  hgt750lemd  35100  hgt750lem2  35104  3exp7  42878  3lexlogpow5ineq1  42879  25or6to4  43031  235t711  43124  ex-decpmul  43125  3cubeslem3l  43475  3cubeslem3r  43476  fmtno2  48360  fmtno3  48361  fmtno4  48362  fmtno5lem4  48366  fmtno5  48367  fmtno4nprmfac193  48384  fmtno5fac  48392  127prm  48409  mod42tp1mod8  48412  ppivalnn4  48437  2exp340mod341  48556  gbowge7  48586  sbgoldbwt  48600  nnsum3primesle9  48617