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

Theorem 6p1e7 10689
Description: 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
6p1e7

Proof of Theorem 6p1e7
StepHypRef Expression
1 df-7 10624 . 2
21eqcomi 2470 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296  1c1 9514   caddc 9516  6c6 10614  7c7 10615
This theorem is referenced by:  9t8e72  11105  s7len  12860  37prm  14606  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem3  14615  1259lem4  14616  1259lem5  14617  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem4  14626  4001prm  14627  log2ublem3  23279  log2ub  23280
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-7 10624
  Copyright terms: Public domain W3C validator