Theorem 7p1e8 12408

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11120   + caddc 11122  7c7 12319  8c8 12320

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-8 12328

This theorem is used by:  7t4e28  12847  9t9e81  12865  s8len  14968  prmlem2  17206  83prm  17209  163prm  17211  317prm  17212  631prm  17213  2503lem2  17224  2503lem3  17225  4001lem2  17228  4001lem3  17229  4001prm  17231  hgt750lem  35107  hgt750lem2  35108  lcmineqlem  42881  1p7e8  43093  3cubeslem3l  43494  3cubeslem3r  43495  resqrtvalex  44448  imsqrtvalex  44449  fmtno5lem4  48385  fmtno4nprmfac193  48403  m3prm  48421  m7prm  48429  nnsum3primesle9  48636  bgoldbtbndlem1  48647