Definition df-4 9374

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 9366	. 2 class 4
2		c3 9365	. . 3 class 3
3		c1 8186	. . 3 class 1
4		caddc 8188	. . 3 class +
5	2, 3, 4	co 6088	. 2 class ( 3 + 1 )
6	1, 5	wceq 1402	1 wff 4 = ( 3 + 1 )

This definition is used by:  4re  9390  4pos  9410  4m1e3  9434  2p2e4  9440  3p1e4  9449  3p2e5  9455  4p4e8  9459  5p4e9  9462  4nn  9479  3lt4  9488  halfpm6th  9536  6p4e10  9863  7p4e11  9867  7p7e14  9870  8p4e12  9873  8p6e14  9875  9p4e13  9880  9p5e14  9881  4t4e16  9890  5t4e20  9893  6t4e24  9897  7t4e28  9902  8t4e32  9908  9t4e36  9915  fz0to4untppr  10547  fzo0to42pr  10654  4bc2eq6  11234  ef4p  12485  ef01bndlem  12547  sincosq4sgn  16073  binom4  16236  ppiublem2  16309  ppiqub  16310  chtqub  16313  bclbnd  16324  bposlem8  16335  lgsdir2lem3  16371