Definition df-5 11944

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 11936	. 2 class 5
2		c4 11935	. . 3 class 4
3		c1 10778	. . 3 class 1
4		caddc 10780	. . 3 class +
5	2, 3, 4	co 7252	. 2 class (4 + 1)
6	1, 5	wceq 1543	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  11964  5re  11965  5cn  11966  5pos  11987  5m1e4  12008  4p1e5  12024  3p2e5  12029  4p2e6  12031  4lt5  12055  5p5e10  12412  6p5e11  12414  7p5e12  12418  8p5e13  12424  8p7e15  12426  9p5e14  12431  9p6e15  12432  5t5e25  12444  6t5e30  12448  7t5e35  12453  8t5e40  12459  9t5e45  12466  fldiv4p1lem1div2  13458  ef01bndlem  15796  prm23lt5  16418  5prm  16713  lt6abl  19386  log2ublem3  25978  ppiublem2  26231  bclbnd  26308  bposlem6  26317  bposlem9  26320  lgsdir2lem3  26355  2lgslem3c  26426  2lgsoddprmlem3c  26440  ex-exp  28690  ex-fac  28691  ex-bc  28692  3lexlogpow5ineq5  39975  aks4d1p1p7  39988  rmydioph  40724  expdiophlem2  40732  stoweidlem13  43417  fmtno5  44870  fmtnofac1  44883  31prm  44910  5odd  45023  sbgoldbo  45100  ackval50  45905