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

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

Proof of Theorem 6p1e7
StepHypRef Expression
1 df-7 10673 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2442 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6305   1c1 9539    + caddc 9541   6c6 10663   7c7 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-7 10673
This theorem is referenced by:  9t8e72  11152  s7len  12976  37prm  15055  163prm  15059  317prm  15060  631prm  15061  1259lem1  15065  1259lem3  15067  1259lem4  15068  1259lem5  15069  2503lem1  15071  2503lem2  15072  2503lem3  15073  2503prm  15074  4001lem1  15075  4001lem4  15078  4001prm  15079  log2ublem3  23739  log2ub  23740  gboge7  38254  bgoldbwt  38268  nnsum3primesle9  38279
  Copyright terms: Public domain W3C validator