Theorem 7p1e8 12052

Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
7p1e8	⊢ (7 + 1) = 8

Proof of Theorem 7p1e8

Step	Hyp	Ref	Expression
1		df-8 11972	. 2 ⊢ 8 = (7 + 1)
2	1	eqcomi 2747	1 ⊢ (7 + 1) = 8

Syntax hints:   = wceq 1539  (class class class)co 7255  1c1 10803   + caddc 10805  7c7 11963  8c8 11964

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-8 11972

This theorem is referenced by:  7t4e28  12477  9t9e81  12495  s8len  14544  prmlem2  16749  83prm  16752  163prm  16754  317prm  16755  631prm  16756  2503lem2  16767  2503lem3  16768  4001lem2  16771  4001lem3  16772  4001prm  16774  hgt750lem  32531  hgt750lem2  32532  lcmineqlem  39988  3cubeslem3l  40424  3cubeslem3r  40425  resqrtvalex  41142  imsqrtvalex  41143  fmtno5lem4  44896  fmtno4nprmfac193  44914  m3prm  44932  m7prm  44940  nnsum3primesle9  45134  bgoldbtbndlem1  45145