Definition df-3 12303

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 12295	. 2 class 3
2		c2 12294	. . 3 class 2
3		c1 11100	. . 3 class 1
4		caddc 11102	. . 3 class +
5	2, 3, 4	co 7410	. 2 class (2 + 1)
6	1, 5	wceq 1568	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  12319  3re  12320  3cn  12321  3m1e2  12367  2p2e4  12374  2p1e3  12381  3p3e6  12391  4p3e7  12393  5p3e8  12396  6p3e9  12399  3t3e9  12407  2lt3  12413  7p3e10  12790  7p6e13  12793  8p3e11  12796  8p5e13  12798  9p3e12  12803  9p4e13  12804  4t3e12  12813  5t3e15  12816  6t3e18  12820  7t3e21  12825  8t3e24  12831  9t3e27  12838  nn01to3  12964  fztpval  13613  fz0to3un2pr  13656  fzo0to42pr  13781  fzo1to4tp  13782  cu2  14235  i3  14238  binom3  14259  fac3  14315  hashtpg  14521  01sqrexlem7  15298  bpoly2  16110  bpoly4  16112  fsumcube  16113  ege2le3  16143  ef4p  16168  cos1bnd  16242  oddprmge3  16758  prmgaplem3  17112  13prm  17175  23prm  17178  43prm  17181  83prm  17182  163prm  17184  lt6abl  19964  cphipval  25381  vitalilem4  25749  itgcnlem  25928  dveflem  26117  sincosq3sgn  26641  sincosq4sgn  26642  tangtx  26646  sincos6thpi  26657  ang180lem2  26951  mcubic  26988  cubic2  26989  binom4  26991  dquartlem2  26993  quart1  26997  quartlem1  26998  log2ublem3  27089  basellem5  27225  basellem8  27228  basellem9  27229  ppi3  27311  cht3  27313  ppiublem1  27342  ppiublem2  27343  ppiub  27344  chtub  27352  bclbnd  27420  bposlem2  27425  bposlem9  27432  lgsdir2lem3  27467  dchrvmasumiflem1  27641  mulog2sumlem2  27675  pntlemk  27746  pntlemo  27747  axlowdimlem3  29260  axlowdimlem13  29270  axlowdimlem16  29273  axlowdimlem17  29274  2wlkdlem1  30240  elwwlks2s3  30266  elwspths2spth  30285  upgr3v3e3cycl  30497  upgr4cycl4dv4e  30502  konigsberglem5  30573  ipval2  31025  stm1add3i  32565  stadd3i  32566  problem2  36112  problem4  36114  sinccvglem  36118  mblfinlem3  38254  heiborlem6  38411  aks4d1p1  42789  2ap1caineq  42858  1p3e4  42972  nicomachus  43019  sn-0ne2  43113  3cubeslem2  43364  3cubeslem3r  43366  rmydioph  43689  rmxdioph  43691  expdiophlem2  43697  expdioph  43698  amgm3d  44873  stoweidlem26  46688  sin3t  47553  cos3t  47554  sin5tlem1  47555  2timesltsq  48060  2timesltsqm1  48061  31prm  48294  lighneallem4b  48306  nprmdvdsfacm1lem2  48318  3odd  48418  sbgoldbo  48497  itcoval3  49390  ackval3  49408