Definition df-6 12229

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 12221	. 2 class 6
2		c5 12220	. . 3 class 5
3		c1 11045	. . 3 class 1
4		caddc 11047	. . 3 class +
5	2, 3, 4	co 7369	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12251  6re  12252  6cn  12253  6pos  12272  6m1e5  12288  5p1e6  12304  3p3e6  12309  4p2e6  12310  5p2e7  12313  5lt6  12338  6p6e12  12699  7p6e13  12703  8p6e14  12709  8p8e16  12711  9p6e15  12716  9p7e16  12717  6t6e36  12733  7t6e42  12738  8t6e48  12744  9t6e54  12751  lt6abl  19801  ppiublem1  27089  ppiublem2  27090  ppiub  27091  bposlem8  27178  lgsdir2lem3  27214  2lgsoddprmlem3d  27300  aks4d1p1p5  42036  rmydioph  42976  expdiophlem2  42984  ceil5half3  47314  stgoldbwt  47750  sbgoldbm  47758