Definition df-4 9203

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 9195	. 2 class 4
2		c3 9194	. . 3 class 3
3		c1 8032	. . 3 class 1
4		caddc 8034	. . 3 class +
5	2, 3, 4	co 6017	. 2 class (3 + 1)
6	1, 5	wceq 1397	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9219  4pos  9239  4m1e3  9263  2p2e4  9269  3p1e4  9278  3p2e5  9284  4p4e8  9288  5p4e9  9291  4nn  9306  3lt4  9315  halfpm6th  9363  6p4e10  9681  7p4e11  9685  7p7e14  9688  8p4e12  9691  8p6e14  9693  9p4e13  9698  9p5e14  9699  4t4e16  9708  5t4e20  9711  6t4e24  9715  7t4e28  9720  8t4e32  9726  9t4e36  9733  fz0to4untppr  10358  fzo0to42pr  10464  4bc2eq6  11035  ef4p  12254  ef01bndlem  12316  sincosq4sgn  15552  binom4  15702  lgsdir2lem3  15758