Definition df-5 11082

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

Assertion

Ref	Expression
df-5	|- 5 = ( 4 + 1 )

Detailed syntax breakdown of Definition df-5

Step	Hyp	Ref	Expression
1		c5 11073	. 2 class 5
2		c4 11072	. . 3 class 4
3		c1 9937	. . 3 class 1
4		caddc 9939	. . 3 class +
5	2, 3, 4	co 6650	. 2 class ( 4 + 1 )
6	1, 5	wceq 1483	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  11099  5pos  11118  5m1e4  11139  4p1e5  11154  3p2e5  11160  4p2e6  11162  5p5e10OLD  11168  5nn  11188  4lt5  11200  5p5e10  11596  6p5e11  11600  6p5e11OLD  11601  7p5e12  11607  8p5e13  11615  8p7e15  11617  9p5e14  11623  9p6e15  11624  5t5e25  11639  5t5e25OLD  11640  6t5e30  11644  6t5e30OLD  11645  7t5e35  11651  8t5e40  11657  8t5e40OLD  11658  9t5e45  11666  fldiv4p1lem1div2  12636  ef01bndlem  14914  prm23lt5  15519  5prm  15815  lt6abl  18296  log2ublem3  24675  ppiublem2  24928  bclbnd  25005  bposlem6  25014  bposlem9  25017  lgsdir2lem3  25052  2lgslem3c  25123  2lgsoddprmlem3c  25137  ex-exp  27307  ex-fac  27308  ex-bc  27309  rmydioph  37581  expdiophlem2  37589  stoweidlem13  40230  fmtno5  41469  fmtnofac1  41482  31prm  41512  5odd  41619  sbgoldbo  41675