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 11122
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 11113 . 2 class 7
2 c6 11112 . . 3 class 6
3 c1 9975 . . 3 class 1
4 caddc 9977 . . 3 class +
52, 3, 4co 6690 . 2 class (6 + 1)
61, 5wceq 1523 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7re  11141  7pos  11158  7m1e6  11179  6p1e7  11194  4p3e7  11201  5p2e7  11203  6p2e8  11207  7nn  11228  6lt7  11247  7p7e14  11647  8p7e15  11655  9p7e16  11663  9p8e17  11664  7t7e49  11691  8t7e56  11699  9t7e63  11706  7prm  15864  17prm  15871  37prm  15875  317prm  15880  log2ublem2  24719  log2ublem3  24720  bclbnd  25050  bposlem8  25061  lgsdir2lem3  25097  2lgslem3d  25169  problem4  31688  rmydioph  37898  expdiophlem2  37906  fmtno5  41794  257prm  41798  2exp7  41839  127prm  41840  7odd  41946  stgoldbwt  41989
  Copyright terms: Public domain W3C validator