Definition df-4 12224

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 12216	. 2 class 4
2		c3 12215	. . 3 class 3
3		c1 11041	. . 3 class 1
4		caddc 11043	. . 3 class +
5	2, 3, 4	co 7370	. 2 class (3 + 1)
6	1, 5	wceq 1542	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12242  4re  12243  4cn  12244  4pos  12266  4m1e3  12283  2p2e4  12289  3p1e4  12299  3p2e5  12305  4p4e8  12309  5p4e9  12312  3lt4  12328  6p4e10  12693  7p4e11  12697  7p7e14  12700  8p4e12  12703  8p6e14  12705  9p4e13  12710  9p5e14  12711  4t4e16  12720  5t4e20  12723  6t4e24  12727  7t4e28  12732  8t4e32  12738  9t4e36  12745  fz0to4untppr  13560  4bc2eq6  14266  bpoly3  15995  bpoly4  15996  fsumcube  15997  ef4p  16052  ef01bndlem  16123  ge2nprmge4  16642  lt6abl  19841  cphipval  25216  sincosq4sgn  26483  binom4  26833  quart1lem  26838  log2cnv  26927  ppiublem2  27187  ppiub  27188  chtub  27196  bclbnd  27264  bposlem8  27275  lgsdir2lem3  27311  3wlkdlem1  30252  ipval2  30801  problem3  35889  aks4d1p1p7  42473  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  lt4addmuld  45697  stoweidlem13  46400  m1modnep2mod  47741  4even  48098  sbgoldbo  48176  ackval40  49082  ackval41a  49083  ackval42  49085