Definition df-4 9187

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 9179	. 2 class 4
2		c3 9178	. . 3 class 3
3		c1 8016	. . 3 class 1
4		caddc 8018	. . 3 class +
5	2, 3, 4	co 6010	. 2 class ( 3 + 1 )
6	1, 5	wceq 1395	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  9203  4pos  9223  4m1e3  9247  2p2e4  9253  3p1e4  9262  3p2e5  9268  4p4e8  9272  5p4e9  9275  4nn  9290  3lt4  9299  halfpm6th  9347  6p4e10  9665  7p4e11  9669  7p7e14  9672  8p4e12  9675  8p6e14  9677  9p4e13  9682  9p5e14  9683  4t4e16  9692  5t4e20  9695  6t4e24  9699  7t4e28  9704  8t4e32  9710  9t4e36  9717  fz0to4untppr  10337  fzo0to42pr  10443  4bc2eq6  11013  ef4p  12226  ef01bndlem  12288  sincosq4sgn  15524  binom4  15674  lgsdir2lem3  15730