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 11558
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 11550 . 2 class 7
2 c6 11549 . . 3 class 6
3 c1 10389 . . 3 class 1
4 caddc 10391 . . 3 class +
52, 3, 4co 7021 . 2 class (6 + 1)
61, 5wceq 1522 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7nn  11582  7re  11583  7cn  11584  7pos  11601  7m1e6  11622  6p1e7  11638  4p3e7  11644  5p2e7  11646  6p2e8  11649  6lt7  11676  7p7e14  12032  8p7e15  12038  9p7e16  12045  9p8e17  12046  7t7e49  12067  8t7e56  12073  9t7e63  12080  7prm  16278  17prm  16284  37prm  16288  317prm  16293  log2ublem2  25212  log2ublem3  25213  bclbnd  25543  bposlem8  25554  lgsdir2lem3  25590  problem4  32526  rmydioph  39122  expdiophlem2  39130  fmtno5  43228  257prm  43232  2exp7  43271  127prm  43272  7odd  43386  stgoldbwt  43450
  Copyright terms: Public domain W3C validator