Definition df-3 12207

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 12199	. 2 class 3
2		c2 12198	. . 3 class 2
3		c1 11025	. . 3 class 1
4		caddc 11027	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (2 + 1)
6	1, 5	wceq 1541	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12222  3re  12223  3cn  12224  3pos  12248  3m1e2  12266  2p2e4  12273  2p1e3  12280  3p3e6  12290  4p3e7  12292  5p3e8  12295  6p3e9  12298  3t3e9  12305  2lt3  12310  7p3e10  12680  7p6e13  12683  8p3e11  12686  8p5e13  12688  9p3e12  12693  9p4e13  12694  4t3e12  12703  5t3e15  12706  6t3e18  12710  7t3e21  12715  8t3e24  12721  9t3e27  12728  nn01to3  12852  fztpval  13500  fz0to3un2pr  13543  fzo0to42pr  13667  fzo1to4tp  13668  cu2  14121  i3  14124  binom3  14145  fac3  14201  hashtpg  14406  01sqrexlem7  15169  bpoly2  15978  bpoly4  15980  fsumcube  15981  ege2le3  16011  ef4p  16036  cos1bnd  16110  oddprmge3  16625  prmgaplem3  16979  13prm  17041  23prm  17044  43prm  17047  83prm  17048  163prm  17050  lt6abl  19822  cphipval  25197  vitalilem4  25566  itgcnlem  25745  dveflem  25937  sincosq3sgn  26463  sincosq4sgn  26464  tangtx  26468  sincos6thpi  26479  ang180lem2  26774  mcubic  26811  cubic2  26812  binom4  26814  dquartlem2  26816  quart1  26820  quartlem1  26821  log2ublem3  26912  basellem5  27049  basellem8  27052  basellem9  27053  ppi3  27135  cht3  27137  ppiublem1  27167  ppiublem2  27168  ppiub  27169  chtub  27177  bclbnd  27245  bposlem2  27250  bposlem9  27257  lgsdir2lem3  27292  dchrvmasumiflem1  27466  mulog2sumlem2  27500  pntlemk  27571  pntlemo  27572  axlowdimlem3  28966  axlowdimlem13  28976  axlowdimlem16  28979  axlowdimlem17  28980  2wlkdlem1  29947  elwwlks2s3  29973  elwspths2spth  29992  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  konigsberglem5  30280  ipval2  30731  stm1add3i  32271  stadd3i  32272  problem2  35809  problem4  35811  sinccvglem  35815  mblfinlem3  37799  heiborlem6  37956  aks4d1p1  42269  2ap1caineq  42338  1p3e4  42456  nicomachus  42509  sn-0ne2  42603  3cubeslem2  42869  3cubeslem3r  42871  rmydioph  43198  rmxdioph  43200  expdiophlem2  43206  expdioph  43207  amgm3d  44382  stoweidlem26  46212  31prm  47785  lighneallem4b  47797  3odd  47896  sbgoldbo  47975  itcoval3  48853  ackval3  48871