Definition df-4 11968

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 11960	. 2 class 4
2		c3 11959	. . 3 class 3
3		c1 10803	. . 3 class 1
4		caddc 10805	. . 3 class +
5	2, 3, 4	co 7255	. 2 class (3 + 1)
6	1, 5	wceq 1539	1 wff 4 = (3 + 1)

This definition is referenced by:  4nn  11986  4re  11987  4cn  11988  4pos  12010  4m1e3  12032  2p2e4  12038  3p1e4  12048  3p2e5  12054  4p4e8  12058  5p4e9  12061  3lt4  12077  halfpm6th  12124  6p4e10  12438  7p4e11  12442  7p7e14  12445  8p4e12  12448  8p6e14  12450  9p4e13  12455  9p5e14  12456  4t4e16  12465  5t4e20  12468  6t4e24  12472  7t4e28  12477  8t4e32  12483  9t4e36  12490  fz0to4untppr  13288  4bc2eq6  13971  bpoly3  15696  bpoly4  15697  fsumcube  15698  ef4p  15750  ef01bndlem  15821  ge2nprmge4  16334  lt6abl  19411  cphipval  24312  sincosq4sgn  25563  binom4  25905  quart1lem  25910  log2cnv  25999  ppiublem2  26256  ppiub  26257  chtub  26265  bclbnd  26333  bposlem8  26344  lgsdir2lem3  26380  3wlkdlem1  28424  ipval2  28970  problem3  33525  aks4d1p1p7  40010  rmydioph  40752  rmxdioph  40754  expdiophlem2  40760  lt4addmuld  42735  stoweidlem13  43444  4even  45049  sbgoldbo  45127  ackval40  45927  ackval41a  45928  ackval42  45930