Definition df-5 9133

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 9125	. 2 class 5
2		c4 9124	. . 3 class 4
3		c1 7961	. . 3 class 1
4		caddc 7963	. . 3 class +
5	2, 3, 4	co 5967	. 2 class ( 4 + 1 )
6	1, 5	wceq 1373	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9150  5pos  9171  5m1e4  9193  4p1e5  9208  3p2e5  9213  4p2e6  9215  5nn  9236  4lt5  9247  5p5e10  9609  6p5e11  9611  7p5e12  9615  8p5e13  9621  8p7e15  9623  9p5e14  9628  9p6e15  9629  5t5e25  9641  6t5e30  9645  7t5e35  9650  8t5e40  9656  9t5e45  9663  fldiv4p1lem1div2  10485  ef01bndlem  12182  prm23lt5  12701  lgsdir2lem3  15622  2lgslem3c  15687  2lgsoddprmlem3c  15701  ex-exp  15863  ex-fac  15864  ex-bc  15865