Definition df-4 12038

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 12030	. 2 class 4
2		c3 12029	. . 3 class 3
3		c1 10873	. . 3 class 1
4		caddc 10875	. . 3 class +
5	2, 3, 4	co 7271	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12056  4re  12057  4cn  12058  4pos  12080  4m1e3  12102  2p2e4  12108  3p1e4  12118  3p2e5  12124  4p4e8  12128  5p4e9  12131  3lt4  12147  halfpm6th  12194  6p4e10  12508  7p4e11  12512  7p7e14  12515  8p4e12  12518  8p6e14  12520  9p4e13  12525  9p5e14  12526  4t4e16  12535  5t4e20  12538  6t4e24  12542  7t4e28  12547  8t4e32  12553  9t4e36  12560  fz0to4untppr  13358  4bc2eq6  14041  bpoly3  15766  bpoly4  15767  fsumcube  15768  ef4p  15820  ef01bndlem  15891  ge2nprmge4  16404  lt6abl  19494  cphipval  24405  sincosq4sgn  25656  binom4  25998  quart1lem  26003  log2cnv  26092  ppiublem2  26349  ppiub  26350  chtub  26358  bclbnd  26426  bposlem8  26437  lgsdir2lem3  26473  3wlkdlem1  28519  ipval2  29065  problem3  33621  aks4d1p1p7  40079  rmydioph  40833  rmxdioph  40835  expdiophlem2  40841  lt4addmuld  42816  stoweidlem13  43525  4even  45130  sbgoldbo  45208  ackval40  46008  ackval41a  46009  ackval42  46011