Definition df-4 12329

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 12321	. 2 class 4
2		c3 12320	. . 3 class 3
3		c1 11159	. . 3 class 1
4		caddc 11161	. . 3 class +
5	2, 3, 4	co 7424	. 2 class (3 + 1)
6	1, 5	wceq 1534	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  12347  4re  12348  4cn  12349  4pos  12371  4m1e3  12393  2p2e4  12399  3p1e4  12409  3p2e5  12415  4p4e8  12419  5p4e9  12422  3lt4  12438  halfpm6th  12485  6p4e10  12801  7p4e11  12805  7p7e14  12808  8p4e12  12811  8p6e14  12813  9p4e13  12818  9p5e14  12819  4t4e16  12828  5t4e20  12831  6t4e24  12835  7t4e28  12840  8t4e32  12846  9t4e36  12853  fz0to4untppr  13658  4bc2eq6  14346  bpoly3  16060  bpoly4  16061  fsumcube  16062  ef4p  16115  ef01bndlem  16186  ge2nprmge4  16702  lt6abl  19893  cphipval  25262  sincosq4sgn  26529  binom4  26878  quart1lem  26883  log2cnv  26972  ppiublem2  27232  ppiub  27233  chtub  27241  bclbnd  27309  bposlem8  27320  lgsdir2lem3  27356  3wlkdlem1  30092  ipval2  30640  problem3  35495  aks4d1p1p7  41773  rmydioph  42672  rmxdioph  42674  expdiophlem2  42680  lt4addmuld  44921  stoweidlem13  45634  4even  47281  sbgoldbo  47359  ackval40  48081  ackval41a  48082  ackval42  48084