Theorem 6p1e7 12263

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

Syntax hints:   = wceq 1541  (class class class)co 7341  1c1 11002   + caddc 11004  6c6 12179  7c7 12180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-7 12188

This theorem is referenced by:  9t8e72  12711  s7len  14804  37prm  17027  163prm  17031  317prm  17032  631prm  17033  1259lem1  17037  1259lem3  17039  1259lem4  17040  1259lem5  17041  2503lem1  17043  2503lem2  17044  2503lem3  17045  2503prm  17046  4001lem1  17047  4001lem4  17050  4001prm  17051  log2ublem3  26880  log2ub  26881  hgt750lemd  34653  hgt750lem2  34657  3exp7  42086  3lexlogpow5ineq1  42087  235t711  42338  ex-decpmul  42339  3cubeslem3l  42719  3cubeslem3r  42720  fmtno2  47581  fmtno3  47582  fmtno4  47583  fmtno5lem4  47587  fmtno5  47588  fmtno4nprmfac193  47605  fmtno5fac  47613  127prm  47630  mod42tp1mod8  47633  2exp340mod341  47764  gbowge7  47794  sbgoldbwt  47808  nnsum3primesle9  47825