Definition df-3 12234

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 12226	. 2 class 3
2		c2 12225	. . 3 class 2
3		c1 11028	. . 3 class 1
4		caddc 11030	. . 3 class +
5	2, 3, 4	co 7356	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12249  3re  12250  3cn  12251  3pos  12275  3m1e2  12293  2p2e4  12300  2p1e3  12307  3p3e6  12317  4p3e7  12319  5p3e8  12322  6p3e9  12325  3t3e9  12332  2lt3  12337  7p3e10  12708  7p6e13  12711  8p3e11  12714  8p5e13  12716  9p3e12  12721  9p4e13  12722  4t3e12  12731  5t3e15  12734  6t3e18  12738  7t3e21  12743  8t3e24  12749  9t3e27  12756  nn01to3  12880  fztpval  13529  fz0to3un2pr  13572  fzo0to42pr  13697  fzo1to4tp  13698  cu2  14151  i3  14154  binom3  14175  fac3  14231  hashtpg  14436  01sqrexlem7  15199  bpoly2  16011  bpoly4  16013  fsumcube  16014  ege2le3  16044  ef4p  16069  cos1bnd  16143  oddprmge3  16659  prmgaplem3  17013  13prm  17075  23prm  17078  43prm  17081  83prm  17082  163prm  17084  lt6abl  19859  cphipval  25198  vitalilem4  25566  itgcnlem  25745  dveflem  25934  sincosq3sgn  26452  sincosq4sgn  26453  tangtx  26457  sincos6thpi  26468  ang180lem2  26762  mcubic  26799  cubic2  26800  binom4  26802  dquartlem2  26804  quart1  26808  quartlem1  26809  log2ublem3  26900  basellem5  27036  basellem8  27039  basellem9  27040  ppi3  27122  cht3  27124  ppiublem1  27153  ppiublem2  27154  ppiub  27155  chtub  27163  bclbnd  27231  bposlem2  27236  bposlem9  27243  lgsdir2lem3  27278  dchrvmasumiflem1  27452  mulog2sumlem2  27486  pntlemk  27557  pntlemo  27558  axlowdimlem3  29001  axlowdimlem13  29011  axlowdimlem16  29014  axlowdimlem17  29015  2wlkdlem1  29981  elwwlks2s3  30007  elwspths2spth  30026  upgr3v3e3cycl  30238  upgr4cycl4dv4e  30243  konigsberglem5  30314  ipval2  30766  stm1add3i  32306  stadd3i  32307  problem2  35836  problem4  35838  sinccvglem  35842  mblfinlem3  37968  heiborlem6  38125  aks4d1p1  42503  2ap1caineq  42572  1p3e4  42685  nicomachus  42732  sn-0ne2  42826  3cubeslem2  43105  3cubeslem3r  43107  rmydioph  43430  rmxdioph  43432  expdiophlem2  43438  expdioph  43439  amgm3d  44614  stoweidlem26  46442  sin3t  47307  cos3t  47308  sin5tlem1  47309  2timesltsq  47814  2timesltsqm1  47815  31prm  48048  lighneallem4b  48060  nprmdvdsfacm1lem2  48072  3odd  48172  sbgoldbo  48251  itcoval3  49129  ackval3  49147