Definition df-5 12252

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 12244	. 2 class 5
2		c4 12243	. . 3 class 4
3		c1 11069	. . 3 class 1
4		caddc 11071	. . 3 class +
5	2, 3, 4	co 7387	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12272  5re  12273  5cn  12274  5pos  12295  5m1e4  12311  4p1e5  12327  3p2e5  12332  4p2e6  12334  4lt5  12358  5p5e10  12720  6p5e11  12722  7p5e12  12726  8p5e13  12732  8p7e15  12734  9p5e14  12739  9p6e15  12740  5t5e25  12752  6t5e30  12756  7t5e35  12761  8t5e40  12767  9t5e45  12774  fldiv4p1lem1div2  13797  ef01bndlem  16152  prm23lt5  16785  5prm  17079  lt6abl  19825  log2ublem3  26858  ppiublem2  27114  bclbnd  27191  bposlem6  27200  bposlem9  27203  lgsdir2lem3  27238  2lgslem3c  27309  2lgsoddprmlem3c  27323  ex-exp  30379  ex-fac  30380  ex-bc  30381  3lexlogpow5ineq5  42048  aks4d1p1p7  42062  rmydioph  43003  expdiophlem2  43011  stoweidlem13  46011  fmtno5  47555  fmtnofac1  47568  31prm  47595  5odd  47708  sbgoldbo  47785  gpgprismgr4cycllem7  48088  gpgprismgr4cycllem9  48090  ackval50  48684