Theorem 6p1e7 12121

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

Syntax hints:   = wceq 1539  (class class class)co 7275  1c1 10872   + caddc 10874  6c6 12032  7c7 12033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-7 12041

This theorem is referenced by:  9t8e72  12565  s7len  14615  37prm  16822  163prm  16826  317prm  16827  631prm  16828  1259lem1  16832  1259lem3  16834  1259lem4  16835  1259lem5  16836  2503lem1  16838  2503lem2  16839  2503lem3  16840  2503prm  16841  4001lem1  16842  4001lem4  16845  4001prm  16846  log2ublem3  26098  log2ub  26099  hgt750lemd  32628  hgt750lem2  32632  3exp7  40061  3lexlogpow5ineq1  40062  235t711  40319  ex-decpmul  40320  3cubeslem3l  40508  3cubeslem3r  40509  fmtno2  45002  fmtno3  45003  fmtno4  45004  fmtno5lem4  45008  fmtno5  45009  fmtno4nprmfac193  45026  fmtno5fac  45034  127prm  45051  mod42tp1mod8  45054  2exp340mod341  45185  gbowge7  45215  sbgoldbwt  45229  nnsum3primesle9  45246