Definition df-3 12406

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 12398	. 2 class 3
2		c2 12397	. . 3 class 2
3		c1 11201	. . 3 class 1
4		caddc 11203	. . 3 class +
5	2, 3, 4	co 7420	. 2 class (2 + 1)
6	1, 5	wceq 1569	1 wff 3 = (2 + 1)

This definition is used by:  3nn  12422  3re  12423  3cn  12424  3m1e2  12470  2p2e4  12477  2p1e3  12484  3p3e6  12494  4p3e7  12496  5p3e8  12499  6p3e9  12502  3t3e9  12510  2lt3  12516  7p3e10  12894  7p6e13  12897  8p3e11  12900  8p5e13  12902  9p3e12  12907  9p4e13  12908  4t3e12  12917  5t3e15  12920  6t3e18  12924  7t3e21  12929  8t3e24  12935  9t3e27  12942  nn01to3  13068  fztpval  13720  fz0to3un2pr  13763  fzo0to42pr  13888  fzo1to4tp  13889  cu2  14343  i3  14347  binom3  14368  fac3  14424  hashtpg  14630  01sqrexlem7  15415  bpoly2  16223  bpoly4  16225  fsumcube  16226  ege2le3  16256  ef4p  16281  cos1bnd  16355  oddprmge3  16876  prmgaplem3  17231  13prm  17294  23prm  17297  43prm  17300  83prm  17301  163prm  17303  lt6abl  20109  cphipval  25564  vitalilem4  25932  itgcnlem  26110  dveflem  26299  sincosq3sgn  26829  sincosq4sgn  26830  tangtx  26834  sincos6thpi  26844  ang180lem2  27138  mcubic  27175  cubic2  27176  binom4  27178  dquartlem2  27180  quart1  27184  quartlem1  27185  log2ublem3  27276  basellem5  27412  basellem9  27416  ppi3  27498  cht3  27500  ppiublem1  27529  ppiublem2  27530  ppiub  27531  chtub  27539  bclbnd  27607  bposlem2  27612  bposlem9  27619  lgsdir2lem3  27654  dchrvmasumiflem1  27828  mulog2sumlem2  27862  pntlemk  27933  pntlemo  27934  axlowdimlem3  29522  axlowdimlem13  29532  axlowdimlem16  29535  axlowdimlem17  29536  2wlkdlem1  30514  elwwlks2s3  30540  elwspths2spth  30559  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  konigsberglem5  30857  ipval2  31309  stm1add3i  32849  stadd3i  32850  problem2  36431  problem4  36433  sinccvglem  36437  mblfinlem3  38578  heiborlem6  38751  aks4d1p1  43127  2ap1caineq  43196  1p3e4  43311  nicomachus  43370  sn-0ne2  43458  3cubeslem2  43696  3cubeslem3r  43698  rmydioph  44021  rmxdioph  44023  expdiophlem2  44029  expdioph  44030  amgm3d  45199  stoweidlem26  47036  sin3t  47917  cos3t  47918  sin5tlem1  47919  goldpolyfactor  47927  2timesltsq  48448  2timesltsqm1  48449  31prm  48682  lighneallem4b  48694  nprmdvdsfacm1lem2  48706  3odd  48806  sbgoldbo  48885  itcoval3  49777  ackval3  49795