Definition df-6 12195

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 12187	. 2 class 6
2		c5 12186	. . 3 class 5
3		c1 11010	. . 3 class 1
4		caddc 11012	. . 3 class +
5	2, 3, 4	co 7349	. 2 class (5 + 1)
6	1, 5	wceq 1540	1 wff 6 = (5 + 1)

This definition is referenced by:  6nn  12217  6re  12218  6cn  12219  6pos  12238  6m1e5  12254  5p1e6  12270  3p3e6  12275  4p2e6  12276  5p2e7  12279  5lt6  12304  6p6e12  12665  7p6e13  12669  8p6e14  12675  8p8e16  12677  9p6e15  12682  9p7e16  12683  6t6e36  12699  7t6e42  12704  8t6e48  12710  9t6e54  12717  lt6abl  19774  ppiublem1  27111  ppiublem2  27112  ppiub  27113  bposlem8  27200  lgsdir2lem3  27236  2lgsoddprmlem3d  27322  aks4d1p1p5  42048  rmydioph  42987  expdiophlem2  42995  ceil5half3  47324  stgoldbwt  47760  sbgoldbm  47768