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 11694
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 11686 . 2 class 7
2 c6 11685 . . 3 class 6
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7145 . 2 class (6 + 1)
61, 5wceq 1528 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7nn  11718  7re  11719  7cn  11720  7pos  11737  7m1e6  11758  6p1e7  11774  4p3e7  11780  5p2e7  11782  6p2e8  11785  6lt7  11812  7p7e14  12166  8p7e15  12172  9p7e16  12179  9p8e17  12180  7t7e49  12201  8t7e56  12207  9t7e63  12214  7prm  16434  17prm  16440  37prm  16444  317prm  16449  log2ublem2  25453  log2ublem3  25454  bclbnd  25784  bposlem8  25795  lgsdir2lem3  25831  problem4  32809  3cubeslem3r  39164  rmydioph  39491  expdiophlem2  39499  fmtno5  43566  257prm  43570  2exp7  43609  127prm  43610  7odd  43724  stgoldbwt  43788
  Copyright terms: Public domain W3C validator