MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-7 Structured version   Visualization version   GIF version

Definition df-7 11365
Description: Define the number 7. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-7 7 = (6 + 1)

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 11357 . 2 class 7
2 c6 11356 . . 3 class 6
3 c1 10218 . . 3 class 1
4 caddc 10220 . . 3 class +
52, 3, 4co 6870 . 2 class (6 + 1)
61, 5wceq 1637 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7re  11383  7pos  11399  7m1e6  11420  6p1e7  11435  4p3e7  11441  5p2e7  11443  6p2e8  11446  7nn  11463  6lt7  11481  7p7e14  11834  8p7e15  11840  9p7e16  11847  9p8e17  11848  7t7e49  11869  8t7e56  11875  9t7e63  11882  7prm  16025  17prm  16031  37prm  16035  317prm  16040  log2ublem2  24884  log2ublem3  24885  bclbnd  25215  bposlem8  25226  lgsdir2lem3  25262  2lgslem3d  25334  problem4  31879  rmydioph  38076  expdiophlem2  38084  fmtno5  42038  257prm  42042  2exp7  42083  127prm  42084  7odd  42190  stgoldbwt  42233
  Copyright terms: Public domain W3C validator