Definition df-4 12258

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 12250	. 2 class 4
2		c3 12249	. . 3 class 3
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7390	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12276  4re  12277  4cn  12278  4pos  12300  4m1e3  12317  2p2e4  12323  3p1e4  12333  3p2e5  12339  4p4e8  12343  5p4e9  12346  3lt4  12362  6p4e10  12728  7p4e11  12732  7p7e14  12735  8p4e12  12738  8p6e14  12740  9p4e13  12745  9p5e14  12746  4t4e16  12755  5t4e20  12758  6t4e24  12762  7t4e28  12767  8t4e32  12773  9t4e36  12780  fz0to4untppr  13598  4bc2eq6  14301  bpoly3  16031  bpoly4  16032  fsumcube  16033  ef4p  16088  ef01bndlem  16159  ge2nprmge4  16678  lt6abl  19832  cphipval  25150  sincosq4sgn  26417  binom4  26767  quart1lem  26772  log2cnv  26861  ppiublem2  27121  ppiub  27122  chtub  27130  bclbnd  27198  bposlem8  27209  lgsdir2lem3  27245  3wlkdlem1  30095  ipval2  30643  problem3  35661  aks4d1p1p7  42069  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  lt4addmuld  45311  stoweidlem13  46018  m1modnep2mod  47357  4even  47714  sbgoldbo  47792  ackval40  48686  ackval41a  48687  ackval42  48689