Definition df-4 12047

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 12039	. 2 class 4
2		c3 12038	. . 3 class 3
3		c1 10881	. . 3 class 1
4		caddc 10883	. . 3 class +
5	2, 3, 4	co 7284	. 2 class (3 + 1)
6	1, 5	wceq 1539	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12065  4re  12066  4cn  12067  4pos  12089  4m1e3  12111  2p2e4  12117  3p1e4  12127  3p2e5  12133  4p4e8  12137  5p4e9  12140  3lt4  12156  halfpm6th  12203  6p4e10  12518  7p4e11  12522  7p7e14  12525  8p4e12  12528  8p6e14  12530  9p4e13  12535  9p5e14  12536  4t4e16  12545  5t4e20  12548  6t4e24  12552  7t4e28  12557  8t4e32  12563  9t4e36  12570  fz0to4untppr  13368  4bc2eq6  14052  bpoly3  15777  bpoly4  15778  fsumcube  15779  ef4p  15831  ef01bndlem  15902  ge2nprmge4  16415  lt6abl  19505  cphipval  24416  sincosq4sgn  25667  binom4  26009  quart1lem  26014  log2cnv  26103  ppiublem2  26360  ppiub  26361  chtub  26369  bclbnd  26437  bposlem8  26448  lgsdir2lem3  26484  3wlkdlem1  28532  ipval2  29078  problem3  33634  aks4d1p1p7  40089  rmydioph  40843  rmxdioph  40845  expdiophlem2  40851  lt4addmuld  42852  stoweidlem13  43561  4even  45172  sbgoldbo  45250  ackval40  46050  ackval41a  46051  ackval42  46053