Definition df-6 12409

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 12401	. 2 class 6
2		c5 12400	. . 3 class 5
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (5 + 1)
6	1, 5	wceq 1569	1 wff 6 = (5 + 1)

This definition is used by:  6nn  12432  6re  12433  6cn  12434  6m1e5  12473  5p1e6  12489  3p3e6  12494  4p2e6  12495  5p2e7  12498  5lt6  12526  6p6e12  12893  7p6e13  12897  8p6e14  12903  8p8e16  12905  9p6e15  12910  9p7e16  12911  6t6e36  12927  7t6e42  12932  8t6e48  12938  9t6e54  12945  lt6abl  20109  ppiublem1  27529  ppiublem2  27530  ppiub  27531  bposlem8  27618  lgsdir2lem3  27654  2lgsoddprmlem3d  27740  aks4d1p1p5  43126  1p6e7  43314  rmydioph  44021  expdiophlem2  44029  ceil5half3  48416  stgoldbwt  48874  sbgoldbm  48882