Theorem 6p1e7 12288

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11027   + caddc 11029  6c6 12204  7c7 12205

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 2123  ax-ext 2708

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

This theorem is referenced by:  9t8e72  12735  s7len  14825  37prm  17048  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem4  17071  4001prm  17072  log2ublem3  26914  log2ub  26915  hgt750lemd  34805  hgt750lem2  34809  3exp7  42307  3lexlogpow5ineq1  42308  235t711  42560  ex-decpmul  42561  3cubeslem3l  42928  3cubeslem3r  42929  fmtno2  47796  fmtno3  47797  fmtno4  47798  fmtno5lem4  47802  fmtno5  47803  fmtno4nprmfac193  47820  fmtno5fac  47828  127prm  47845  mod42tp1mod8  47848  2exp340mod341  47979  gbowge7  48009  sbgoldbwt  48023  nnsum3primesle9  48040