Definition df-3 9181

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 9173	. 2 class 3
2		c2 9172	. . 3 class 2
3		c1 8011	. . 3 class 1
4		caddc 8013	. . 3 class +
5	2, 3, 4	co 6007	. 2 class (2 + 1)
6	1, 5	wceq 1395	1 wff 3 = (2 + 1)

This definition is referenced by:  3re  9195  3pos  9215  3m1e2  9241  2p2e4  9248  2p1e3  9255  3p3e6  9264  4p3e7  9266  5p3e8  9269  6p3e9  9272  3t3e9  9279  3nn  9284  2lt3  9292  7p3e10  9663  7p6e13  9666  8p3e11  9669  8p5e13  9671  9p3e12  9676  9p4e13  9677  4t3e12  9686  5t3e15  9689  6t3e18  9693  7t3e21  9698  8t3e24  9704  9t3e27  9711  nn01to3  9824  fztpval  10291  fz0to3un2pr  10331  fz0to4untppr  10332  fzo0to42pr  10438  cu2  10872  i3  10875  binom3  10891  fac3  10966  ege2le3  12197  ef4p  12220  cos1bnd  12285  3prm  12665  oddprmge3  12672  dveflem  15415  sincosq3sgn  15517  sincosq4sgn  15518  tangtx  15527  sincos6thpi  15531  binom4  15668  lgsdir2lem3  15724