Theorem 7p1e8 12303

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 12228	. 2 ⊢ 8 = (7 + 1)
2	1	eqcomi 2746	1 ⊢ (7 + 1) = 8

Syntax hints:   = wceq 1542  (class class class)co 7370  1c1 11041   + caddc 11043  7c7 12219  8c8 12220

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-8 12228

This theorem is referenced by:  7t4e28  12732  9t9e81  12750  s8len  14840  prmlem2  17061  83prm  17064  163prm  17066  317prm  17067  631prm  17068  2503lem2  17079  2503lem3  17080  4001lem2  17083  4001lem3  17084  4001prm  17086  hgt750lem  34835  hgt750lem2  34836  lcmineqlem  42451  3cubeslem3l  43072  3cubeslem3r  43073  resqrtvalex  44030  imsqrtvalex  44031  fmtno5lem4  47945  fmtno4nprmfac193  47963  m3prm  47981  m7prm  47989  nnsum3primesle9  48183  bgoldbtbndlem1  48194