Theorem 7p1e8 12389

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11101   + caddc 11103  7c7 12300  8c8 12301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-8 12309

This theorem is referenced by:  7t4e28  12827  9t9e81  12845  s8len  14940  prmlem2  17180  83prm  17183  163prm  17185  317prm  17186  631prm  17187  2503lem2  17198  2503lem3  17199  4001lem2  17202  4001lem3  17203  4001prm  17205  hgt750lem  34983  hgt750lem2  34984  lcmineqlem  42743  3cubeslem3l  43343  3cubeslem3r  43344  resqrtvalex  44297  imsqrtvalex  44298  fmtno5lem4  48231  fmtno4nprmfac193  48249  m3prm  48267  m7prm  48275  nnsum3primesle9  48482  bgoldbtbndlem1  48493