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

Theorem 6p1e7 10745
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 10680 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2435 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437  (class class class)co 6305   1c1 9547    + caddc 9549   6c6 10670   7c7 10671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-7 10680
This theorem is referenced by:  9t8e72  11159  s7len  12997  37prm  15091  163prm  15095  317prm  15096  631prm  15097  1259lem1  15101  1259lem3  15103  1259lem4  15104  1259lem5  15105  2503lem1  15107  2503lem2  15108  2503lem3  15109  2503prm  15110  4001lem1  15111  4001lem4  15114  4001prm  15115  log2ublem3  23872  log2ub  23873  gboge7  38734  bgoldbwt  38748  nnsum3primesle9  38759
  Copyright terms: Public domain W3C validator