Definition df-3 12242

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 12234	. 2 class 3
2		c2 12233	. . 3 class 2
3		c1 11036	. . 3 class 1
4		caddc 11038	. . 3 class +
5	2, 3, 4	co 7364	. 2 class (2 + 1)
6	1, 5	wceq 1542	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12257  3re  12258  3cn  12259  3pos  12283  3m1e2  12301  2p2e4  12308  2p1e3  12315  3p3e6  12325  4p3e7  12327  5p3e8  12330  6p3e9  12333  3t3e9  12340  2lt3  12345  7p3e10  12716  7p6e13  12719  8p3e11  12722  8p5e13  12724  9p3e12  12729  9p4e13  12730  4t3e12  12739  5t3e15  12742  6t3e18  12746  7t3e21  12751  8t3e24  12757  9t3e27  12764  nn01to3  12888  fztpval  13537  fz0to3un2pr  13580  fzo0to42pr  13705  fzo1to4tp  13706  cu2  14159  i3  14162  binom3  14183  fac3  14239  hashtpg  14444  01sqrexlem7  15207  bpoly2  16019  bpoly4  16021  fsumcube  16022  ege2le3  16052  ef4p  16077  cos1bnd  16151  oddprmge3  16667  prmgaplem3  17021  13prm  17083  23prm  17086  43prm  17089  83prm  17090  163prm  17092  lt6abl  19867  cphipval  25207  vitalilem4  25575  itgcnlem  25754  dveflem  25943  sincosq3sgn  26461  sincosq4sgn  26462  tangtx  26466  sincos6thpi  26477  ang180lem2  26771  mcubic  26808  cubic2  26809  binom4  26811  dquartlem2  26813  quart1  26817  quartlem1  26818  log2ublem3  26909  basellem5  27045  basellem8  27048  basellem9  27049  ppi3  27131  cht3  27133  ppiublem1  27162  ppiublem2  27163  ppiub  27164  chtub  27172  bclbnd  27240  bposlem2  27245  bposlem9  27252  lgsdir2lem3  27287  dchrvmasumiflem1  27461  mulog2sumlem2  27495  pntlemk  27566  pntlemo  27567  axlowdimlem3  29010  axlowdimlem13  29020  axlowdimlem16  29023  axlowdimlem17  29024  2wlkdlem1  29990  elwwlks2s3  30016  elwspths2spth  30035  upgr3v3e3cycl  30247  upgr4cycl4dv4e  30252  konigsberglem5  30323  ipval2  30775  stm1add3i  32315  stadd3i  32316  problem2  35845  problem4  35847  sinccvglem  35851  mblfinlem3  37977  heiborlem6  38134  aks4d1p1  42512  2ap1caineq  42581  1p3e4  42694  nicomachus  42741  sn-0ne2  42835  3cubeslem2  43114  3cubeslem3r  43116  rmydioph  43439  rmxdioph  43441  expdiophlem2  43447  expdioph  43448  amgm3d  44623  stoweidlem26  46451  sin3t  47314  cos3t  47315  sin5tlem1  47316  2timesltsq  47817  2timesltsqm1  47818  31prm  48051  lighneallem4b  48063  nprmdvdsfacm1lem2  48075  3odd  48175  sbgoldbo  48254  itcoval3  49132  ackval3  49150