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

Theorem 6p1e7 10664
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 10599 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2480 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6284   1c1 9493    + caddc 9495   6c6 10589   7c7 10590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-7 10599
This theorem is referenced by:  9t8e72  11077  s7len  12823  37prm  14464  163prm  14468  317prm  14469  631prm  14470  1259lem1  14471  1259lem3  14473  1259lem4  14474  1259lem5  14475  2503lem1  14477  2503lem2  14478  2503lem3  14479  2503prm  14480  4001lem1  14481  4001lem4  14484  4001prm  14485  log2ublem3  23035  log2ub  23036
  Copyright terms: Public domain W3C validator