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

Theorem 6p1e7 10112
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 10068 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2442 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6084   1c1 8996    + caddc 8998   6c6 10058   7c7 10059
This theorem is referenced by:  9t8e72  10488  s7len  11864  37prm  13448  163prm  13452  317prm  13453  631prm  13454  1259lem1  13455  1259lem3  13457  1259lem4  13458  1259lem5  13459  2503lem1  13461  2503lem2  13462  2503lem3  13463  2503prm  13464  4001lem1  13465  4001lem4  13468  4001prm  13469  log2ublem3  20793  log2ub  20794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-7 10068
  Copyright terms: Public domain W3C validator