Definition df-4 12274

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 12266	. 2 class 4
2		c3 12265	. . 3 class 3
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12292  4re  12293  4cn  12294  4pos  12316  4m1e3  12338  2p2e4  12344  3p1e4  12354  3p2e5  12360  4p4e8  12364  5p4e9  12367  3lt4  12383  halfpm6th  12430  6p4e10  12746  7p4e11  12750  7p7e14  12753  8p4e12  12756  8p6e14  12758  9p4e13  12763  9p5e14  12764  4t4e16  12773  5t4e20  12776  6t4e24  12780  7t4e28  12785  8t4e32  12791  9t4e36  12798  fz0to4untppr  13601  4bc2eq6  14286  bpoly3  15999  bpoly4  16000  fsumcube  16001  ef4p  16053  ef01bndlem  16124  ge2nprmge4  16635  lt6abl  19758  cphipval  24752  sincosq4sgn  26003  binom4  26345  quart1lem  26350  log2cnv  26439  ppiublem2  26696  ppiub  26697  chtub  26705  bclbnd  26773  bposlem8  26784  lgsdir2lem3  26820  3wlkdlem1  29402  ipval2  29948  problem3  34641  aks4d1p1p7  40928  rmydioph  41739  rmxdioph  41741  expdiophlem2  41747  lt4addmuld  44003  stoweidlem13  44716  4even  46364  sbgoldbo  46442  ackval40  47333  ackval41a  47334  ackval42  47336