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

Definition df-7 10624
Description: Define the number 7. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-7

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 10615 . 2
2 c6 10614 . . 3
3 c1 9514 . . 3
4 caddc 9516 . . 3
52, 3, 4co 6296 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  7re  10643  7pos  10660  6p1e7  10689  4p3e7  10696  5p2e7  10698  6p2e8  10702  7nn  10723  6lt7  10742  7p7e14  11059  8p7e15  11064  9p7e16  11071  9p8e17  11072  7t7e49  11091  8t7e56  11097  9t7e63  11104  7prm  14596  17prm  14602  37prm  14606  317prm  14611  log2ublem2  23278  log2ublem3  23279  bclbnd  23555  bposlem8  23566  lgsdir2lem3  23600  problem4  29022  rmydioph  30956  expdiophlem2  30964
  Copyright terms: Public domain W3C validator