Definition df-4 9194

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 9186	. 2 class 4
2		c3 9185	. . 3 class 3
3		c1 8023	. . 3 class 1
4		caddc 8025	. . 3 class +
5	2, 3, 4	co 6013	. 2 class (3 + 1)
6	1, 5	wceq 1395	1 wff 4 = (3 + 1)

This definition is referenced by:  4re  9210  4pos  9230  4m1e3  9254  2p2e4  9260  3p1e4  9269  3p2e5  9275  4p4e8  9279  5p4e9  9282  4nn  9297  3lt4  9306  halfpm6th  9354  6p4e10  9672  7p4e11  9676  7p7e14  9679  8p4e12  9682  8p6e14  9684  9p4e13  9689  9p5e14  9690  4t4e16  9699  5t4e20  9702  6t4e24  9706  7t4e28  9711  8t4e32  9717  9t4e36  9724  fz0to4untppr  10349  fzo0to42pr  10455  4bc2eq6  11026  ef4p  12245  ef01bndlem  12307  sincosq4sgn  15543  binom4  15693  lgsdir2lem3  15749