Theorem 6p1e7 12530

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  6c6 12441  7c7 12442

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  9t8e72  12987  s7len  15096  37prm  17343  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem4  17366  4001prm  17367  log2ublem3  27333  log2ub  27334  hgt750lemd  35388  hgt750lem2  35392  3exp7  43369  3lexlogpow5ineq1  43370  25or6to4  43522  1p6e7  43579  235t711  43628  ex-decpmul  43629  3cubeslem3l  43962  3cubeslem3r  43963  fmtno2  48908  fmtno3  48909  fmtno4  48910  fmtno5lem4  48914  fmtno5  48915  fmtno4nprmfac193  48932  fmtno5fac  48940  127prm  48957  mod42tp1mod8  48960  ppivalnn4  48985  2exp340mod341  49104  gbowge7  49134  sbgoldbwt  49148  nnsum3primesle9  49165