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

Theorem 6p1e7 10071
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 10027 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2416 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6048   1c1 8955    + caddc 8957   6c6 10017   7c7 10018
This theorem is referenced by:  9t8e72  10447  s7len  11822  37prm  13406  163prm  13410  317prm  13411  631prm  13412  1259lem1  13413  1259lem3  13415  1259lem4  13416  1259lem5  13417  2503lem1  13419  2503lem2  13420  2503lem3  13421  2503prm  13422  4001lem1  13423  4001lem4  13426  4001prm  13427  log2ublem3  20749  log2ub  20750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-cleq 2405  df-7 10027
  Copyright terms: Public domain W3C validator