Definition df-3 12375

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 12367	. 2 class 3
2		c2 12366	. . 3 class 2
3		c1 11172	. . 3 class 1
4		caddc 11174	. . 3 class +
5	2, 3, 4	co 7408	. 2 class (2 + 1)
6	1, 5	wceq 1570	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12391  3re  12392  3cn  12393  3m1e2  12439  2p2e4  12446  2p1e3  12453  3p3e6  12463  4p3e7  12465  5p3e8  12468  6p3e9  12471  3t3e9  12479  2lt3  12485  7p3e10  12863  7p6e13  12866  8p3e11  12869  8p5e13  12871  9p3e12  12876  9p4e13  12877  4t3e12  12886  5t3e15  12889  6t3e18  12893  7t3e21  12898  8t3e24  12904  9t3e27  12911  nn01to3  13037  fztpval  13688  fz0to3un2pr  13731  fzo0to42pr  13856  fzo1to4tp  13857  cu2  14311  i3  14314  binom3  14335  fac3  14391  hashtpg  14597  01sqrexlem7  15382  bpoly2  16190  bpoly4  16192  fsumcube  16193  ege2le3  16223  ef4p  16248  cos1bnd  16322  oddprmge3  16838  prmgaplem3  17192  13prm  17255  23prm  17258  43prm  17261  83prm  17262  163prm  17264  lt6abl  20070  cphipval  25525  vitalilem4  25893  itgcnlem  26071  dveflem  26260  sincosq3sgn  26792  sincosq4sgn  26793  tangtx  26797  sincos6thpi  26807  ang180lem2  27101  mcubic  27138  cubic2  27139  binom4  27141  dquartlem2  27143  quart1  27147  quartlem1  27148  log2ublem3  27239  basellem5  27375  basellem9  27379  ppi3  27461  cht3  27463  ppiublem1  27492  ppiublem2  27493  ppiub  27494  chtub  27502  bclbnd  27570  bposlem2  27575  bposlem9  27582  lgsdir2lem3  27617  dchrvmasumiflem1  27791  mulog2sumlem2  27825  pntlemk  27896  pntlemo  27897  axlowdimlem3  29455  axlowdimlem13  29465  axlowdimlem16  29468  axlowdimlem17  29469  2wlkdlem1  30447  elwwlks2s3  30473  elwspths2spth  30492  upgr3v3e3cycl  30714  upgr4cycl4dv4e  30719  konigsberglem5  30790  ipval2  31242  stm1add3i  32782  stadd3i  32783  problem2  36352  problem4  36354  sinccvglem  36358  mblfinlem3  38497  heiborlem6  38670  aks4d1p1  43046  2ap1caineq  43115  1p3e4  43230  nicomachus  43291  sn-0ne2  43385  3cubeslem2  43634  3cubeslem3r  43636  rmydioph  43959  rmxdioph  43961  expdiophlem2  43967  expdioph  43968  amgm3d  45143  stoweidlem26  46958  sin3t  47839  cos3t  47840  sin5tlem1  47841  goldpolyfactor  47849  2timesltsq  48370  2timesltsqm1  48371  31prm  48604  lighneallem4b  48616  nprmdvdsfacm1lem2  48628  3odd  48728  sbgoldbo  48807  itcoval3  49699  ackval3  49717