Definition df-3 12189

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 12181	. 2 class 3
2		c2 12180	. . 3 class 2
3		c1 11007	. . 3 class 1
4		caddc 11009	. . 3 class +
5	2, 3, 4	co 7346	. 2 class (2 + 1)
6	1, 5	wceq 1541	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12204  3re  12205  3cn  12206  3pos  12230  3m1e2  12248  2p2e4  12255  2p1e3  12262  3p3e6  12272  4p3e7  12274  5p3e8  12277  6p3e9  12280  3t3e9  12287  2lt3  12292  7p3e10  12663  7p6e13  12666  8p3e11  12669  8p5e13  12671  9p3e12  12676  9p4e13  12677  4t3e12  12686  5t3e15  12689  6t3e18  12693  7t3e21  12698  8t3e24  12704  9t3e27  12711  nn01to3  12839  fztpval  13486  fz0to3un2pr  13529  fzo0to42pr  13653  fzo1to4tp  13654  cu2  14107  i3  14110  binom3  14131  fac3  14187  hashtpg  14392  01sqrexlem7  15155  bpoly2  15964  bpoly4  15966  fsumcube  15967  ege2le3  15997  ef4p  16022  cos1bnd  16096  oddprmge3  16611  prmgaplem3  16965  13prm  17027  23prm  17030  43prm  17033  83prm  17034  163prm  17036  lt6abl  19807  cphipval  25170  vitalilem4  25539  itgcnlem  25718  dveflem  25910  sincosq3sgn  26436  sincosq4sgn  26437  tangtx  26441  sincos6thpi  26452  ang180lem2  26747  mcubic  26784  cubic2  26785  binom4  26787  dquartlem2  26789  quart1  26793  quartlem1  26794  log2ublem3  26885  basellem5  27022  basellem8  27025  basellem9  27026  ppi3  27108  cht3  27110  ppiublem1  27140  ppiublem2  27141  ppiub  27142  chtub  27150  bclbnd  27218  bposlem2  27223  bposlem9  27230  lgsdir2lem3  27265  dchrvmasumiflem1  27439  mulog2sumlem2  27473  pntlemk  27544  pntlemo  27545  axlowdimlem3  28922  axlowdimlem13  28932  axlowdimlem16  28935  axlowdimlem17  28936  2wlkdlem1  29903  elwwlks2s3  29929  elwspths2spth  29948  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  konigsberglem5  30236  ipval2  30687  stm1add3i  32227  stadd3i  32228  problem2  35710  problem4  35712  sinccvglem  35716  mblfinlem3  37707  heiborlem6  37864  aks4d1p1  42117  2ap1caineq  42186  1p3e4  42300  nicomachus  42353  sn-0ne2  42447  3cubeslem2  42726  3cubeslem3r  42728  rmydioph  43055  rmxdioph  43057  expdiophlem2  43063  expdioph  43064  amgm3d  44240  stoweidlem26  46072  31prm  47636  lighneallem4b  47648  3odd  47747  sbgoldbo  47826  itcoval3  48705  ackval3  48723