Definition df-5 11284

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 11275	. 2 class 5
2		c4 11274	. . 3 class 4
3		c1 10139	. . 3 class 1
4		caddc 10141	. . 3 class +
5	2, 3, 4	co 6793	. 2 class (4 + 1)
6	1, 5	wceq 1631	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  11301  5pos  11320  5m1e4  11341  4p1e5  11356  3p2e5  11362  4p2e6  11364  5p5e10OLD  11370  5nn  11390  4lt5  11402  5p5e10  11797  6p5e11  11801  6p5e11OLD  11802  7p5e12  11808  8p5e13  11816  8p7e15  11818  9p5e14  11824  9p6e15  11825  5t5e25  11840  5t5e25OLD  11841  6t5e30  11845  6t5e30OLD  11846  7t5e35  11852  8t5e40  11858  8t5e40OLD  11859  9t5e45  11867  fldiv4p1lem1div2  12844  ef01bndlem  15120  prm23lt5  15726  5prm  16022  lt6abl  18503  log2ublem3  24896  ppiublem2  25149  bclbnd  25226  bposlem6  25235  bposlem9  25238  lgsdir2lem3  25273  2lgslem3c  25344  2lgsoddprmlem3c  25358  ex-exp  27649  ex-fac  27650  ex-bc  27651  rmydioph  38107  expdiophlem2  38115  stoweidlem13  40747  fmtno5  41997  fmtnofac1  42010  31prm  42040  5odd  42147  sbgoldbo  42203