Definition df-4 8167

Description: Define the number 4. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-4	|- 4 = ( 3 + 1 )

Detailed syntax breakdown of Definition df-4

Step	Hyp	Ref	Expression
1		c4 8158	. 2 class 4
2		c3 8157	. . 3 class 3
3		c1 7044	. . 3 class 1
4		caddc 7046	. . 3 class +
5	2, 3, 4	co 5543	. 2 class ( 3 + 1 )
6	1, 5	wceq 1285	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8183  4pos  8203  2p2e4  8226  3p1e4  8234  3p2e5  8240  4p4e8  8244  5p4e9  8247  4nn  8262  3lt4  8271  halfpm6th  8318  6p4e10  8629  7p4e11  8633  7p7e14  8636  8p4e12  8639  8p6e14  8641  9p4e13  8646  9p5e14  8647  4t4e16  8656  5t4e20  8659  6t4e24  8663  7t4e28  8668  8t4e32  8674  9t4e36  8681  fzo0to42pr  9306  4bc2eq6  9798