Definition df-4 12227

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 12219	. 2 class 4
2		c3 12218	. . 3 class 3
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (3 + 1)
6	1, 5	wceq 1540	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12245  4re  12246  4cn  12247  4pos  12269  4m1e3  12286  2p2e4  12292  3p1e4  12302  3p2e5  12308  4p4e8  12312  5p4e9  12315  3lt4  12331  6p4e10  12697  7p4e11  12701  7p7e14  12704  8p4e12  12707  8p6e14  12709  9p4e13  12714  9p5e14  12715  4t4e16  12724  5t4e20  12727  6t4e24  12731  7t4e28  12736  8t4e32  12742  9t4e36  12749  fz0to4untppr  13567  4bc2eq6  14270  bpoly3  16000  bpoly4  16001  fsumcube  16002  ef4p  16057  ef01bndlem  16128  ge2nprmge4  16647  lt6abl  19801  cphipval  25119  sincosq4sgn  26386  binom4  26736  quart1lem  26741  log2cnv  26830  ppiublem2  27090  ppiub  27091  chtub  27099  bclbnd  27167  bposlem8  27178  lgsdir2lem3  27214  3wlkdlem1  30061  ipval2  30609  problem3  35627  aks4d1p1p7  42035  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  lt4addmuld  45277  stoweidlem13  45984  m1modnep2mod  47326  4even  47683  sbgoldbo  47761  ackval40  48655  ackval41a  48656  ackval42  48658