Theorem 7p1e8 12368

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

Syntax hints:   = wceq 1562  (class class class)co 7398  1c1 11076   + caddc 11078  7c7 12279  8c8 12280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-8 12288

This theorem is referenced by:  7t4e28  12806  9t9e81  12824  s8len  14918  prmlem2  17158  83prm  17161  163prm  17163  317prm  17164  631prm  17165  2503lem2  17176  2503lem3  17177  4001lem2  17180  4001lem3  17181  4001prm  17183  hgt750lem  34947  hgt750lem2  34948  lcmineqlem  42674  3cubeslem3l  43272  3cubeslem3r  43273  resqrtvalex  44226  imsqrtvalex  44227  fmtno5lem4  48170  fmtno4nprmfac193  48188  m3prm  48206  m7prm  48214  nnsum3primesle9  48421  bgoldbtbndlem1  48432