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

Step	Hyp	Ref	Expression
1		c7 10615	. 2
2		c6 10614	. . 3
3		c1 9514	. . 3
4		caddc 9516	. . 3
5	2, 3, 4	co 6296	. 2
6	1, 5	wceq 1395	1

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