Definition df-6 12330

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 12322	. 2 class 6
2		c5 12321	. . 3 class 5
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (5 + 1)
6	1, 5	wceq 1536	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12352  6re  12353  6cn  12354  6pos  12373  6m1e5  12394  5p1e6  12410  3p3e6  12415  4p2e6  12416  5p2e7  12419  5lt6  12444  6p6e12  12804  7p6e13  12808  8p6e14  12814  8p8e16  12816  9p6e15  12821  9p7e16  12822  6t6e36  12838  7t6e42  12843  8t6e48  12849  9t6e54  12856  lt6abl  19927  ppiublem1  27260  ppiublem2  27261  ppiub  27262  bposlem8  27349  lgsdir2lem3  27385  2lgsoddprmlem3d  27471  aks4d1p1p5  42056  rmydioph  43002  expdiophlem2  43010  ceil5half3  47279  stgoldbwt  47700  sbgoldbm  47708