Definition df-4 12315

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 12307	. 2 class 4
2		c3 12306	. . 3 class 3
3		c1 11111	. . 3 class 1
4		caddc 11113	. . 3 class +
5	2, 3, 4	co 7416	. 2 class (3 + 1)
6	1, 5	wceq 1570	1 wff 4 = (3 + 1)

This definition is used by:  4nn  12334  4re  12335  4cn  12336  4m1e3  12379  2p2e4  12385  3p1e4  12395  3p2e5  12401  4p4e8  12405  5p4e9  12408  3lt4  12427  6p4e10  12798  7p4e11  12802  7p7e14  12805  8p4e12  12808  8p6e14  12810  9p4e13  12815  9p5e14  12816  4t4e16  12825  5t4e20  12828  6t4e24  12832  7t4e28  12837  8t4e32  12843  9t4e36  12850  fz0to4untppr  13669  4bc2eq6  14376  bpoly3  16122  bpoly4  16123  fsumcube  16124  ef4p  16179  ef01bndlem  16250  ge2nprmge4  16770  lt6abl  19975  cphipval  25417  sincosq4sgn  26681  binom4  27030  quart1lem  27035  log2cnv  27124  ppiublem2  27382  ppiub  27383  chtub  27391  bclbnd  27459  bposlem8  27470  lgsdir2lem3  27506  3wlkdlem1  30525  ipval2  31074  problem3  36171  aks4d1p1p7  42873  rmydioph  43773  rmxdioph  43775  expdiophlem2  43781  lt4addmuld  46057  stoweidlem13  46759  sin5tlem2  47643  m1modnep2mod  48127  4even  48506  sbgoldbo  48584  ackval40  49505  ackval41a  49506  ackval42  49508