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

Theorem 6p1e7 9867
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 9825 . 2  |-  7  =  ( 6  +  1 )
21eqcomi 2300 1  |-  ( 6  +  1 )  =  7
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874   1c1 8754    + caddc 8756   6c6 9815   7c7 9816
This theorem is referenced by:  9t8e72  10241  s7len  11561  37prm  13138  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem3  13147  1259lem4  13148  1259lem5  13149  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem4  13158  4001prm  13159  log2ublem3  20260  log2ub  20261
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-7 9825
  Copyright terms: Public domain W3C validator