Definition df-5 9044

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 9036	. 2 class 5
2		c4 9035	. . 3 class 4
3		c1 7873	. . 3 class 1
4		caddc 7875	. . 3 class +
5	2, 3, 4	co 5918	. 2 class ( 4 + 1 )
6	1, 5	wceq 1364	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9061  5pos  9082  5m1e4  9104  4p1e5  9118  3p2e5  9123  4p2e6  9125  5nn  9146  4lt5  9157  5p5e10  9518  6p5e11  9520  7p5e12  9524  8p5e13  9530  8p7e15  9532  9p5e14  9537  9p6e15  9538  5t5e25  9550  6t5e30  9554  7t5e35  9559  8t5e40  9565  9t5e45  9572  fldiv4p1lem1div2  10374  ef01bndlem  11899  prm23lt5  12401  lgsdir2lem3  15146  2lgsoddprmlem3c  15197  ex-exp  15219  ex-fac  15220  ex-bc  15221