Theorem 6p1e7 12051

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

Syntax hints:   = wceq 1539  (class class class)co 7255  1c1 10803   + caddc 10805  6c6 11962  7c7 11963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-7 11971

This theorem is referenced by:  9t8e72  12494  s7len  14543  37prm  16750  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem3  16762  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem4  16773  4001prm  16774  log2ublem3  26003  log2ub  26004  hgt750lemd  32528  hgt750lem2  32532  3exp7  39989  3lexlogpow5ineq1  39990  235t711  40240  ex-decpmul  40241  3cubeslem3l  40424  3cubeslem3r  40425  fmtno2  44890  fmtno3  44891  fmtno4  44892  fmtno5lem4  44896  fmtno5  44897  fmtno4nprmfac193  44914  fmtno5fac  44922  127prm  44939  mod42tp1mod8  44942  2exp340mod341  45073  gbowge7  45103  sbgoldbwt  45117  nnsum3primesle9  45134