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

Theorem 6p1e7 9943
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 9899 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2362 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff set class
Syntax hints:    = wceq 1642  (class class class)co 5945   1c1 8828    + caddc 8830   6c6 9889   7c7 9890
This theorem is referenced by:  9t8e72  10317  s7len  11641  37prm  13219  163prm  13223  317prm  13224  631prm  13225  1259lem1  13226  1259lem3  13228  1259lem4  13229  1259lem5  13230  2503lem1  13232  2503lem2  13233  2503lem3  13234  2503prm  13235  4001lem1  13236  4001lem4  13239  4001prm  13240  log2ublem3  20355  log2ub  20356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-cleq 2351  df-7 9899
  Copyright terms: Public domain W3C validator