Definition df-5 9100

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 9092	. 2 class 5
2		c4 9091	. . 3 class 4
3		c1 7928	. . 3 class 1
4		caddc 7930	. . 3 class +
5	2, 3, 4	co 5946	. 2 class ( 4 + 1 )
6	1, 5	wceq 1373	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9117  5pos  9138  5m1e4  9160  4p1e5  9175  3p2e5  9180  4p2e6  9182  5nn  9203  4lt5  9214  5p5e10  9576  6p5e11  9578  7p5e12  9582  8p5e13  9588  8p7e15  9590  9p5e14  9595  9p6e15  9596  5t5e25  9608  6t5e30  9612  7t5e35  9617  8t5e40  9623  9t5e45  9630  fldiv4p1lem1div2  10450  ef01bndlem  12100  prm23lt5  12619  lgsdir2lem3  15540  2lgslem3c  15605  2lgsoddprmlem3c  15619  ex-exp  15700  ex-fac  15701  ex-bc  15702