Definition df-5 12328

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 12320	. 2 class 5
2		c4 12319	. . 3 class 4
3		c1 11152	. . 3 class 1
4		caddc 11154	. . 3 class +
5	2, 3, 4	co 7429	. 2 class (4 + 1)
6	1, 5	wceq 1540	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12348  5re  12349  5cn  12350  5pos  12371  5m1e4  12392  4p1e5  12408  3p2e5  12413  4p2e6  12415  4lt5  12439  5p5e10  12800  6p5e11  12802  7p5e12  12806  8p5e13  12812  8p7e15  12814  9p5e14  12819  9p6e15  12820  5t5e25  12832  6t5e30  12836  7t5e35  12841  8t5e40  12847  9t5e45  12854  fldiv4p1lem1div2  13871  ef01bndlem  16216  prm23lt5  16848  5prm  17142  lt6abl  19909  log2ublem3  26981  ppiublem2  27237  bclbnd  27314  bposlem6  27323  bposlem9  27326  lgsdir2lem3  27361  2lgslem3c  27432  2lgsoddprmlem3c  27446  ex-exp  30459  ex-fac  30460  ex-bc  30461  3lexlogpow5ineq5  42054  aks4d1p1p7  42068  rmydioph  43019  expdiophlem2  43027  stoweidlem13  46019  fmtno5  47535  fmtnofac1  47548  31prm  47575  5odd  47688  sbgoldbo  47765  ackval50  48610