Definition df-5 12432

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 12424	. 2 class 5
2		c4 12423	. . 3 class 4
3		c1 11225	. . 3 class 1
4		caddc 11227	. . 3 class +
5	2, 3, 4	co 7440	. 2 class (4 + 1)
6	1, 5	wceq 1570	1 wff 5 = (4 + 1)

This definition is used by:  5nn  12453  5re  12454  5cn  12455  5m1e4  12496  4p1e5  12512  3p2e5  12517  4p2e6  12519  4lt5  12546  5p5e10  12914  6p5e11  12916  7p5e12  12920  8p5e13  12926  8p7e15  12928  9p5e14  12933  9p6e15  12934  5t5e25  12946  6t5e30  12950  7t5e35  12955  8t5e40  12961  9t5e45  12968  fldiv4p1lem1div2  13999  ef01bndlem  16378  prm23lt5  17018  5prm  17312  lt6abl  20136  log2ublem3  27303  ppiublem2  27557  bclbnd  27634  bposlem6  27643  bposlem9  27646  lgsdir2lem3  27681  2lgslem3c  27752  2lgsoddprmlem3c  27766  ex-exp  31078  ex-fac  31079  ex-bc  31080  3lexlogpow5ineq5  43301  aks4d1p1p7  43315  1p5e6  43503  4p5e9  43515  rmydioph  44212  expdiophlem2  44220  stoweidlem13  47226  cos5t  48128  goldpolyfactor  48130  goldratval  48139  fmtno5  48845  fmtnofac1  48858  31prm  48885  5odd  49011  sbgoldbo  49088  gpgprismgr4cycllem7  49402  gpgprismgr4cycllem9  49404  ackval50  50013