Definition df-5 9368

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 9360	. 2 class 5
2		c4 9359	. . 3 class 4
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class ( 4 + 1 )
6	1, 5	wceq 1402	1 wff 5 = ( 4 + 1 )

This definition is used by:  5re  9385  5pos  9406  5m1e4  9428  4p1e5  9443  3p2e5  9448  4p2e6  9450  5nn  9473  4lt5  9484  5p5e10  9856  6p5e11  9858  7p5e12  9862  8p5e13  9868  8p7e15  9870  9p5e14  9875  9p6e15  9876  5t5e25  9888  6t5e30  9892  7t5e35  9897  8t5e40  9903  9t5e45  9910  fldiv4p1lem1div2  10753  ef01bndlem  12539  prm23lt5  13062  5prm  13243  log2ublem3  16142  ppiublem2  16193  bclbnd  16205  lgsdir2lem3  16247  2lgslem3c  16312  2lgsoddprmlem3c  16326  ex-exp  16839  ex-fac  16840  ex-bc  16841