Definition df-3 8938

Description: Define the number 3. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
df-3	|- 3 = ( 2 + 1 )

Detailed syntax breakdown of Definition df-3

Step	Hyp	Ref	Expression
1		c3 8930	. 2 class 3
2		c2 8929	. . 3 class 2
3		c1 7775	. . 3 class 1
4		caddc 7777	. . 3 class +
5	2, 3, 4	co 5853	. 2 class ( 2 + 1 )
6	1, 5	wceq 1348	1 wff 3 = ( 2 + 1 )

This definition is referenced by:  3re  8952  3pos  8972  3m1e2  8998  2p2e4  9005  2p1e3  9011  3p3e6  9020  4p3e7  9022  5p3e8  9025  6p3e9  9028  3t3e9  9035  3nn  9040  2lt3  9048  7p3e10  9417  7p6e13  9420  8p3e11  9423  8p5e13  9425  9p3e12  9430  9p4e13  9431  4t3e12  9440  5t3e15  9443  6t3e18  9447  7t3e21  9452  8t3e24  9458  9t3e27  9465  nn01to3  9576  fztpval  10039  fz0to3un2pr  10079  fz0to4untppr  10080  fzo0to42pr  10176  cu2  10574  i3  10577  binom3  10593  fac3  10666  ege2le3  11634  ef4p  11657  cos1bnd  11722  3prm  12082  oddprmge3  12089  dveflem  13481  sincosq3sgn  13543  sincosq4sgn  13544  tangtx  13553  sincos6thpi  13557  binom4  13691  lgsdir2lem3  13725