Definition df-3 12273

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 12265	. 2 class 3
2		c2 12264	. . 3 class 2
3		c1 11108	. . 3 class 1
4		caddc 11110	. . 3 class +
5	2, 3, 4	co 7406	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12288  3re  12289  3cn  12290  3pos  12314  3m1e2  12337  2p2e4  12344  2p1e3  12351  3p3e6  12361  4p3e7  12363  5p3e8  12366  6p3e9  12369  3t3e9  12376  2lt3  12381  7p3e10  12749  7p6e13  12752  8p3e11  12755  8p5e13  12757  9p3e12  12762  9p4e13  12763  4t3e12  12772  5t3e15  12775  6t3e18  12779  7t3e21  12784  8t3e24  12790  9t3e27  12797  nn01to3  12922  fztpval  13560  fz0to3un2pr  13600  fz0to4untppr  13601  fzo0to42pr  13716  fzo1to4tp  13717  cu2  14161  i3  14164  binom3  14184  fac3  14237  hashtpg  14443  01sqrexlem7  15192  bpoly2  15998  bpoly4  16000  fsumcube  16001  ege2le3  16030  ef4p  16053  cos1bnd  16127  oddprmge3  16634  prmgaplem3  16983  13prm  17046  23prm  17049  43prm  17052  83prm  17053  163prm  17055  lt6abl  19758  cphipval  24752  vitalilem4  25120  itgcnlem  25299  dveflem  25488  sincosq3sgn  26002  sincosq4sgn  26003  tangtx  26007  sincos6thpi  26017  ang180lem2  26305  mcubic  26342  cubic2  26343  binom4  26345  dquartlem2  26347  quart1  26351  quartlem1  26352  log2ublem3  26443  basellem5  26579  basellem8  26582  basellem9  26583  ppi3  26665  cht3  26667  ppiublem1  26695  ppiublem2  26696  ppiub  26697  chtub  26705  bclbnd  26773  bposlem2  26778  bposlem9  26785  lgsdir2lem3  26820  dchrvmasumiflem1  26994  mulog2sumlem2  27028  pntlemk  27099  pntlemo  27100  axlowdimlem3  28192  axlowdimlem13  28202  axlowdimlem16  28205  axlowdimlem17  28206  2wlkdlem1  29169  elwwlks2s3  29195  elwspths2spth  29211  upgr3v3e3cycl  29423  upgr4cycl4dv4e  29428  konigsberglem5  29499  ipval2  29948  stm1add3i  31488  stadd3i  31489  problem2  34640  problem4  34642  sinccvglem  34646  mblfinlem3  36516  heiborlem6  36673  aks4d1p1  40930  2ap1caineq  40950  fac2xp3  41009  nicomachus  41206  sn-0ne2  41276  3cubeslem2  41409  3cubeslem3r  41411  rmydioph  41739  rmxdioph  41741  expdiophlem2  41747  expdioph  41748  amgm3d  42937  stoweidlem26  44729  31prm  46252  lighneallem4b  46264  3odd  46363  sbgoldbo  46442  itcoval3  47305  ackval3  47323