Definition df-5 12285

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 12277	. 2 class 5
2		c4 12276	. . 3 class 4
3		c1 11076	. . 3 class 1
4		caddc 11078	. . 3 class +
5	2, 3, 4	co 7398	. 2 class (4 + 1)
6	1, 5	wceq 1562	1 wff 5 = (4 + 1)

This definition is referenced by:  5nn  12306  5re  12307  5cn  12308  5m1e4  12349  4p1e5  12365  3p2e5  12370  4p2e6  12372  4lt5  12399  5p5e10  12766  6p5e11  12768  7p5e12  12772  8p5e13  12778  8p7e15  12780  9p5e14  12785  9p6e15  12786  5t5e25  12798  6t5e30  12802  7t5e35  12807  8t5e40  12813  9t5e45  12820  fldiv4p1lem1div2  13847  ef01bndlem  16218  prm23lt5  16852  5prm  17146  lt6abl  19937  log2ublem3  27015  ppiublem2  27269  bclbnd  27346  bposlem6  27355  bposlem9  27358  lgsdir2lem3  27393  2lgslem3c  27464  2lgsoddprmlem3c  27478  ex-exp  30654  ex-fac  30655  ex-bc  30656  3lexlogpow5ineq5  42682  aks4d1p1p7  42696  rmydioph  43596  expdiophlem2  43604  stoweidlem13  46592  cos5t  47478  fmtno5  48171  fmtnofac1  48184  31prm  48211  5odd  48337  sbgoldbo  48414  gpgprismgr4cycllem7  48728  gpgprismgr4cycllem9  48730  ackval50  49325