Definition df-5 9172

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 9164	. 2 class 5
2		c4 9163	. . 3 class 4
3		c1 8000	. . 3 class 1
4		caddc 8002	. . 3 class +
5	2, 3, 4	co 6001	. 2 class ( 4 + 1 )
6	1, 5	wceq 1395	1 wff 5 = ( 4 + 1 )

This definition is referenced by:  5re  9189  5pos  9210  5m1e4  9232  4p1e5  9247  3p2e5  9252  4p2e6  9254  5nn  9275  4lt5  9286  5p5e10  9648  6p5e11  9650  7p5e12  9654  8p5e13  9660  8p7e15  9662  9p5e14  9667  9p6e15  9668  5t5e25  9680  6t5e30  9684  7t5e35  9689  8t5e40  9695  9t5e45  9702  fldiv4p1lem1div2  10525  ef01bndlem  12267  prm23lt5  12786  lgsdir2lem3  15709  2lgslem3c  15774  2lgsoddprmlem3c  15788  ex-exp  16091  ex-fac  16092  ex-bc  16093