Definition df-5 9205

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 9197	. 2 class 5
2		c4 9196	. . 3 class 4
3		c1 8033	. . 3 class 1
4		caddc 8035	. . 3 class +
5	2, 3, 4	co 6018	. 2 class (4 + 1)
6	1, 5	wceq 1397	1 wff 5 = (4 + 1)

This definition is referenced by:  5re  9222  5pos  9243  5m1e4  9265  4p1e5  9280  3p2e5  9285  4p2e6  9287  5nn  9308  4lt5  9319  5p5e10  9681  6p5e11  9683  7p5e12  9687  8p5e13  9693  8p7e15  9695  9p5e14  9700  9p6e15  9701  5t5e25  9713  6t5e30  9717  7t5e35  9722  8t5e40  9728  9t5e45  9735  fldiv4p1lem1div2  10566  ef01bndlem  12335  prm23lt5  12854  lgsdir2lem3  15778  2lgslem3c  15843  2lgsoddprmlem3c  15857  ex-exp  16370  ex-fac  16371  ex-bc  16372