Definition df-5 12329

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 12321	. 2 class 5
2		c4 12320	. . 3 class 4
3		c1 11153	. . 3 class 1
4		caddc 11155	. . 3 class +
5	2, 3, 4	co 7430	. 2 class (4 + 1)
6	1, 5	wceq 1536	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12349  5re  12350  5cn  12351  5pos  12372  5m1e4  12393  4p1e5  12409  3p2e5  12414  4p2e6  12416  4lt5  12440  5p5e10  12801  6p5e11  12803  7p5e12  12807  8p5e13  12813  8p7e15  12815  9p5e14  12820  9p6e15  12821  5t5e25  12833  6t5e30  12837  7t5e35  12842  8t5e40  12848  9t5e45  12855  fldiv4p1lem1div2  13871  ef01bndlem  16216  prm23lt5  16847  5prm  17142  lt6abl  19927  log2ublem3  27005  ppiublem2  27261  bclbnd  27338  bposlem6  27347  bposlem9  27350  lgsdir2lem3  27385  2lgslem3c  27456  2lgsoddprmlem3c  27470  ex-exp  30478  ex-fac  30479  ex-bc  30480  3lexlogpow5ineq5  42041  aks4d1p1p7  42055  rmydioph  43002  expdiophlem2  43010  stoweidlem13  45968  fmtno5  47481  fmtnofac1  47494  31prm  47521  5odd  47634  sbgoldbo  47711  ackval50  48547