Definition df-4 12235

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 12227	. 2 class 4
2		c3 12226	. . 3 class 3
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12253  4re  12254  4cn  12255  4pos  12277  4m1e3  12294  2p2e4  12300  3p1e4  12310  3p2e5  12316  4p4e8  12320  5p4e9  12323  3lt4  12339  6p4e10  12705  7p4e11  12709  7p7e14  12712  8p4e12  12715  8p6e14  12717  9p4e13  12722  9p5e14  12723  4t4e16  12732  5t4e20  12735  6t4e24  12739  7t4e28  12744  8t4e32  12750  9t4e36  12757  fz0to4untppr  13573  4bc2eq6  14280  bpoly3  16012  bpoly4  16013  fsumcube  16014  ef4p  16069  ef01bndlem  16140  ge2nprmge4  16660  lt6abl  19859  cphipval  25198  sincosq4sgn  26453  binom4  26802  quart1lem  26807  log2cnv  26896  ppiublem2  27154  ppiub  27155  chtub  27163  bclbnd  27231  bposlem8  27242  lgsdir2lem3  27278  3wlkdlem1  30217  ipval2  30766  problem3  35837  aks4d1p1p7  42501  rmydioph  43430  rmxdioph  43432  expdiophlem2  43438  lt4addmuld  45727  stoweidlem13  46429  sin5tlem2  47310  m1modnep2mod  47794  4even  48173  sbgoldbo  48251  ackval40  49157  ackval41a  49158  ackval42  49160