Definition df-7 10377

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 10368	. 2
2		c6 10367	. . 3
3		c1 9275	. . 3
4		caddc 9277	. . 3
5	2, 3, 4	co 6086	. 2
6	1, 5	wceq 1369	1

This definition is referenced by:  7re  10396  7pos  10413  6p1e7  10442  4p3e7  10449  5p2e7  10451  6p2e8  10455  7nn  10476  6lt7  10495  7p7e14  10802  8p7e15  10807  9p7e16  10814  9p8e17  10815  7t7e49  10834  8t7e56  10840  9t7e63  10847  7prm  14130  17prm  14136  37prm  14140  317prm  14145  log2ublem2  22322  log2ublem3  22323  bclbnd  22599  bposlem8  22610  lgsdir2lem3  22644  problem4  27270  rmydioph  29334  expdiophlem2  29342