Definition df-5 8910

Description: Define the number 5. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-5	|- 5 = ( 4 + 1 )

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 8902	. 2 class 5
2		c4 8901	. . 3 class 4
3		c1 7745	. . 3 class 1
4		caddc 7747	. . 3 class +
5	2, 3, 4	co 5836	. 2 class ( 4 + 1 )
6	1, 5	wceq 1342	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  8927  5pos  8948  5m1e4  8970  4p1e5  8984  3p2e5  8989  4p2e6  8991  5nn  9012  4lt5  9023  5p5e10  9383  6p5e11  9385  7p5e12  9389  8p5e13  9395  8p7e15  9397  9p5e14  9402  9p6e15  9403  5t5e25  9415  6t5e30  9419  7t5e35  9424  8t5e40  9430  9t5e45  9437  fldiv4p1lem1div2  10230  ef01bndlem  11683  prm23lt5  12172  ex-exp  13445  ex-fac  13446  ex-bc  13447