Definition df-3 8908

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 8900	. 2 class 3
2		c2 8899	. . 3 class 2
3		c1 7745	. . 3 class 1
4		caddc 7747	. . 3 class +
5	2, 3, 4	co 5836	. 2 class (2 + 1)
6	1, 5	wceq 1342	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  8922  3pos  8942  3m1e2  8968  2p2e4  8975  2p1e3  8981  3p3e6  8990  4p3e7  8992  5p3e8  8995  6p3e9  8998  3t3e9  9005  3nn  9010  2lt3  9018  7p3e10  9387  7p6e13  9390  8p3e11  9393  8p5e13  9395  9p3e12  9400  9p4e13  9401  4t3e12  9410  5t3e15  9413  6t3e18  9417  7t3e21  9422  8t3e24  9428  9t3e27  9435  nn01to3  9546  fztpval  10008  fz0to3un2pr  10048  fz0to4untppr  10049  fzo0to42pr  10145  cu2  10543  i3  10546  binom3  10561  fac3  10634  ege2le3  11598  ef4p  11621  cos1bnd  11686  3prm  12039  oddprmge3  12046  dveflem  13228  sincosq3sgn  13290  sincosq4sgn  13291  tangtx  13300  sincos6thpi  13304  binom4  13438