Definition df-5 11704

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 11696	. 2 class 5
2		c4 11695	. . 3 class 4
3		c1 10538	. . 3 class 1
4		caddc 10540	. . 3 class +
5	2, 3, 4	co 7156	. 2 class (4 + 1)
6	1, 5	wceq 1537	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  11724  5re  11725  5cn  11726  5pos  11747  5m1e4  11768  4p1e5  11784  3p2e5  11789  4p2e6  11791  4lt5  11815  5p5e10  12170  6p5e11  12172  7p5e12  12176  8p5e13  12182  8p7e15  12184  9p5e14  12189  9p6e15  12190  5t5e25  12202  6t5e30  12206  7t5e35  12211  8t5e40  12217  9t5e45  12224  fldiv4p1lem1div2  13206  ef01bndlem  15537  prm23lt5  16151  5prm  16442  lt6abl  19015  log2ublem3  25526  ppiublem2  25779  bclbnd  25856  bposlem6  25865  bposlem9  25868  lgsdir2lem3  25903  2lgslem3c  25974  2lgsoddprmlem3c  25988  ex-exp  28229  ex-fac  28230  ex-bc  28231  rmydioph  39660  expdiophlem2  39668  stoweidlem13  42347  fmtno5  43768  fmtnofac1  43781  31prm  43809  5odd  43924  sbgoldbo  44001