Definition df-4 9171

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 9163	. 2 class 4
2		c3 9162	. . 3 class 3
3		c1 8000	. . 3 class 1
4		caddc 8002	. . 3 class +
5	2, 3, 4	co 6001	. 2 class ( 3 + 1 )
6	1, 5	wceq 1395	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9187  4pos  9207  4m1e3  9231  2p2e4  9237  3p1e4  9246  3p2e5  9252  4p4e8  9256  5p4e9  9259  4nn  9274  3lt4  9283  halfpm6th  9331  6p4e10  9649  7p4e11  9653  7p7e14  9656  8p4e12  9659  8p6e14  9661  9p4e13  9666  9p5e14  9667  4t4e16  9676  5t4e20  9679  6t4e24  9683  7t4e28  9688  8t4e32  9694  9t4e36  9701  fz0to4untppr  10320  fzo0to42pr  10426  4bc2eq6  10996  ef4p  12205  ef01bndlem  12267  sincosq4sgn  15503  binom4  15653  lgsdir2lem3  15709