MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  7p1e8 Unicode version

Theorem 7p1e8 10690
Description: 7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
7p1e8

Proof of Theorem 7p1e8
StepHypRef Expression
1 df-8 10625 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  7c7 10615  8c8 10616
This theorem is referenced by:  7t4e28  11088  9t9e81  11106  s8len  12861  prmlem2  14605  83prm  14608  163prm  14610  317prm  14611  631prm  14612  2503lem2  14620  2503lem3  14621  4001lem2  14624  4001lem3  14625  4001prm  14627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-8 10625
  Copyright terms: Public domain W3C validator