Definition df-4 8421

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 8412	. 2 class 4
2		c3 8411	. . 3 class 3
3		c1 7298	. . 3 class 1
4		caddc 7300	. . 3 class +
5	2, 3, 4	co 5615	. 2 class ( 3 + 1 )
6	1, 5	wceq 1287	1 wff 4 = ( 3 + 1 )

This definition is referenced by:  4re  8437  4pos  8457  2p2e4  8480  3p1e4  8488  3p2e5  8494  4p4e8  8498  5p4e9  8501  4nn  8516  3lt4  8525  halfpm6th  8572  6p4e10  8883  7p4e11  8887  7p7e14  8890  8p4e12  8893  8p6e14  8895  9p4e13  8900  9p5e14  8901  4t4e16  8910  5t4e20  8913  6t4e24  8917  7t4e28  8922  8t4e32  8928  9t4e36  8935  fzo0to42pr  9562  4bc2eq6  10082