Definition df-3 9078

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 9070	. 2 class 3
2		c2 9069	. . 3 class 2
3		c1 7908	. . 3 class 1
4		caddc 7910	. . 3 class +
5	2, 3, 4	co 5934	. 2 class (2 + 1)
6	1, 5	wceq 1372	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9092  3pos  9112  3m1e2  9138  2p2e4  9145  2p1e3  9152  3p3e6  9161  4p3e7  9163  5p3e8  9166  6p3e9  9169  3t3e9  9176  3nn  9181  2lt3  9189  7p3e10  9560  7p6e13  9563  8p3e11  9566  8p5e13  9568  9p3e12  9573  9p4e13  9574  4t3e12  9583  5t3e15  9586  6t3e18  9590  7t3e21  9595  8t3e24  9601  9t3e27  9608  nn01to3  9720  fztpval  10187  fz0to3un2pr  10227  fz0to4untppr  10228  fzo0to42pr  10330  cu2  10764  i3  10767  binom3  10783  fac3  10858  ege2le3  11901  ef4p  11924  cos1bnd  11989  3prm  12369  oddprmge3  12376  dveflem  15116  sincosq3sgn  15218  sincosq4sgn  15219  tangtx  15228  sincos6thpi  15232  binom4  15369  lgsdir2lem3  15425