Definition df-6 12433

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

Assertion

Ref	Expression
df-6	⊢ 6 = (5 + 1)

Detailed syntax breakdown of Definition df-6

Step	Hyp	Ref	Expression
1		c6 12425	. 2 class 6
2		c5 12424	. . 3 class 5
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (5 + 1)
6	1, 5	wceq 1570	1 wff 6 = (5 + 1)

This definition is used by:  6nn  12456  6re  12457  6cn  12458  6m1e5  12497  5p1e6  12513  3p3e6  12518  4p2e6  12519  5p2e7  12522  5lt6  12550  6p6e12  12917  7p6e13  12921  8p6e14  12927  8p8e16  12929  9p6e15  12934  9p7e16  12935  6t6e36  12951  7t6e42  12956  8t6e48  12962  9t6e54  12969  lt6abl  20136  ppiublem1  27556  ppiublem2  27557  ppiub  27558  bposlem8  27645  lgsdir2lem3  27681  2lgsoddprmlem3d  27767  aks4d1p1p5  43316  1p6e7  43504  rmydioph  44212  expdiophlem2  44220  ceil5half3  48619  stgoldbwt  49077  sbgoldbm  49085