Definition df-3 12330

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 12322	. 2 class 3
2		c2 12321	. . 3 class 2
3		c1 11156	. . 3 class 1
4		caddc 11158	. . 3 class +
5	2, 3, 4	co 7431	. 2 class (2 + 1)
6	1, 5	wceq 1540	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12345  3re  12346  3cn  12347  3pos  12371  3m1e2  12394  2p2e4  12401  2p1e3  12408  3p3e6  12418  4p3e7  12420  5p3e8  12423  6p3e9  12426  3t3e9  12433  2lt3  12438  7p3e10  12808  7p6e13  12811  8p3e11  12814  8p5e13  12816  9p3e12  12821  9p4e13  12822  4t3e12  12831  5t3e15  12834  6t3e18  12838  7t3e21  12843  8t3e24  12849  9t3e27  12856  nn01to3  12983  fztpval  13626  fz0to3un2pr  13669  fzo0to42pr  13792  fzo1to4tp  13793  cu2  14239  i3  14242  binom3  14263  fac3  14319  hashtpg  14524  01sqrexlem7  15287  bpoly2  16093  bpoly4  16095  fsumcube  16096  ege2le3  16126  ef4p  16149  cos1bnd  16223  oddprmge3  16737  prmgaplem3  17091  13prm  17153  23prm  17156  43prm  17159  83prm  17160  163prm  17162  lt6abl  19913  cphipval  25277  vitalilem4  25646  itgcnlem  25825  dveflem  26017  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sincos6thpi  26558  ang180lem2  26853  mcubic  26890  cubic2  26891  binom4  26893  dquartlem2  26895  quart1  26899  quartlem1  26900  log2ublem3  26991  basellem5  27128  basellem8  27131  basellem9  27132  ppi3  27214  cht3  27216  ppiublem1  27246  ppiublem2  27247  ppiub  27248  chtub  27256  bclbnd  27324  bposlem2  27329  bposlem9  27336  lgsdir2lem3  27371  dchrvmasumiflem1  27545  mulog2sumlem2  27579  pntlemk  27650  pntlemo  27651  axlowdimlem3  28959  axlowdimlem13  28969  axlowdimlem16  28972  axlowdimlem17  28973  2wlkdlem1  29945  elwwlks2s3  29971  elwspths2spth  29987  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsberglem5  30275  ipval2  30726  stm1add3i  32266  stadd3i  32267  problem2  35671  problem4  35673  sinccvglem  35677  mblfinlem3  37666  heiborlem6  37823  aks4d1p1  42077  2ap1caineq  42146  fac2xp3  42240  nicomachus  42346  sn-0ne2  42436  3cubeslem2  42696  3cubeslem3r  42698  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  amgm3d  44212  stoweidlem26  46041  31prm  47584  lighneallem4b  47596  3odd  47695  sbgoldbo  47774  itcoval3  48586  ackval3  48604