Definition df-4 9132

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 9124	. 2 class 4
2		c3 9123	. . 3 class 3
3		c1 7961	. . 3 class 1
4		caddc 7963	. . 3 class +
5	2, 3, 4	co 5967	. 2 class ( 3 + 1 )
6	1, 5	wceq 1373	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9148  4pos  9168  4m1e3  9192  2p2e4  9198  3p1e4  9207  3p2e5  9213  4p4e8  9217  5p4e9  9220  4nn  9235  3lt4  9244  halfpm6th  9292  6p4e10  9610  7p4e11  9614  7p7e14  9617  8p4e12  9620  8p6e14  9622  9p4e13  9627  9p5e14  9628  4t4e16  9637  5t4e20  9640  6t4e24  9644  7t4e28  9649  8t4e32  9655  9t4e36  9662  fz0to4untppr  10281  fzo0to42pr  10386  4bc2eq6  10956  ef4p  12120  ef01bndlem  12182  sincosq4sgn  15416  binom4  15566  lgsdir2lem3  15622