Theorem 6p1e7 12483

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  6c6 12394  7c7 12395

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 2733

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

This theorem is used by:  9t8e72  12940  s7len  15046  37prm  17292  163prm  17296  317prm  17297  631prm  17298  1259lem1  17302  1259lem3  17304  1259lem4  17305  1259lem5  17306  2503lem1  17308  2503lem2  17309  2503lem3  17310  2503prm  17311  4001lem1  17312  4001lem4  17315  4001prm  17316  log2ublem3  27269  log2ub  27270  hgt750lemd  35270  hgt750lem2  35274  3exp7  43083  3lexlogpow5ineq1  43084  25or6to4  43236  1p6e7  43293  235t711  43342  ex-decpmul  43343  3cubeslem3l  43676  3cubeslem3r  43677  fmtno2  48604  fmtno3  48605  fmtno4  48606  fmtno5lem4  48610  fmtno5  48611  fmtno4nprmfac193  48628  fmtno5fac  48636  127prm  48653  mod42tp1mod8  48656  ppivalnn4  48681  2exp340mod341  48800  gbowge7  48830  sbgoldbwt  48844  nnsum3primesle9  48861