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

Theorem 6p1e7 11358
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 11286 . 2 7 = (6 + 1)
21eqcomi 2780 1 (6 + 1) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  (class class class)co 6793  1c1 10139   + caddc 10141  6c6 11276  7c7 11277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-7 11286
This theorem is referenced by:  9t8e72  11870  s7len  13856  37prm  16035  163prm  16039  317prm  16040  631prm  16041  1259lem1  16045  1259lem3  16047  1259lem4  16048  1259lem5  16049  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem4  16058  4001prm  16059  log2ublem3  24896  log2ub  24897  hgt750lemd  31066  hgt750lem2  31070  fmtno2  41990  fmtno3  41991  fmtno4  41992  fmtno5lem4  41996  fmtno5  41997  fmtno4nprmfac193  42014  fmtno5fac  42022  127prm  42043  mod42tp1mod8  42047  gbowge7  42179  sbgoldbwt  42193  nnsum3primesle9  42210
  Copyright terms: Public domain W3C validator