Definition df-3 9364

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 9356	. 2 class 3
2		c2 9355	. . 3 class 2
3		c1 8180	. . 3 class 1
4		caddc 8182	. . 3 class +
5	2, 3, 4	co 6085	. 2 class (2 + 1)
6	1, 5	wceq 1402	1 wff 3 = (2 + 1)

This definition is used by:  3re  9378  3pos  9398  3m1e2  9424  2p2e4  9431  2p1e3  9438  3p3e6  9447  4p3e7  9449  5p3e8  9452  6p3e9  9455  3t3e9  9462  3nn  9467  2lt3  9475  7p3e10  9851  7p6e13  9854  8p3e11  9857  8p5e13  9859  9p3e12  9864  9p4e13  9865  4t3e12  9874  5t3e15  9877  6t3e18  9881  7t3e21  9886  8t3e24  9892  9t3e27  9899  nn01to3  10017  fztpval  10490  fz0to3un2pr  10530  fz0to4untppr  10531  fzo0to42pr  10638  cu2  11075  i3  11078  binom3  11094  fac3  11170  ege2le3  12438  ef4p  12461  cos1bnd  12526  3prm  12906  oddprmge3  12913  dveflem  15827  sincosq3sgn  15929  sincosq4sgn  15930  tangtx  15939  sincos6thpi  15943  binom4  16081  log2ublem3  16085  lgsdir2lem3  16149  konigsberglem5  16733