Theorem 6p1e7 12324

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  6c6 12240  7c7 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  9t8e72  12772  s7len  14864  37prm  17091  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26912  log2ub  26913  hgt750lemd  34792  hgt750lem2  34796  3exp7  42492  3lexlogpow5ineq1  42493  235t711  42737  ex-decpmul  42738  3cubeslem3l  43118  3cubeslem3r  43119  fmtno2  48013  fmtno3  48014  fmtno4  48015  fmtno5lem4  48019  fmtno5  48020  fmtno4nprmfac193  48037  fmtno5fac  48045  127prm  48062  mod42tp1mod8  48065  ppivalnn4  48090  2exp340mod341  48209  gbowge7  48239  sbgoldbwt  48253  nnsum3primesle9  48270