Definition df-3 11942

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 11934	. 2 class 3
2		c2 11933	. . 3 class 2
3		c1 10778	. . 3 class 1
4		caddc 10780	. . 3 class +
5	2, 3, 4	co 7252	. 2 class (2 + 1)
6	1, 5	wceq 1543	1 wff 3 = (2 + 1)

This definition is referenced by:  3nn  11957  3re  11958  3cn  11959  3pos  11983  3m1e2  12006  2p2e4  12013  2p1e3  12020  3p3e6  12030  4p3e7  12032  5p3e8  12035  6p3e9  12038  3t3e9  12045  2lt3  12050  7p3e10  12416  7p6e13  12419  8p3e11  12422  8p5e13  12424  9p3e12  12429  9p4e13  12430  4t3e12  12439  5t3e15  12442  6t3e18  12446  7t3e21  12451  8t3e24  12457  9t3e27  12464  nn01to3  12585  fztpval  13222  fz0to3un2pr  13262  fz0to4untppr  13263  fzo0to42pr  13377  fzo1to4tp  13378  cu2  13820  i3  13823  binom3  13842  fac3  13897  hashtpg  14102  sqrlem7  14863  bpoly2  15670  bpoly4  15672  fsumcube  15673  ege2le3  15702  ef4p  15725  cos1bnd  15799  oddprmge3  16308  prmgaplem3  16657  13prm  16720  23prm  16723  43prm  16726  83prm  16727  163prm  16729  lt6abl  19386  cphipval  24287  vitalilem4  24655  itgcnlem  24834  dveflem  25023  sincosq3sgn  25537  sincosq4sgn  25538  tangtx  25542  sincos6thpi  25552  ang180lem2  25840  mcubic  25877  cubic2  25878  binom4  25880  dquartlem2  25882  quart1  25886  quartlem1  25887  log2ublem3  25978  basellem5  26114  basellem8  26117  basellem9  26118  ppi3  26200  cht3  26202  ppiublem1  26230  ppiublem2  26231  ppiub  26232  chtub  26240  bclbnd  26308  bposlem2  26313  bposlem9  26320  lgsdir2lem3  26355  dchrvmasumiflem1  26529  mulog2sumlem2  26563  pntlemk  26634  pntlemo  26635  axlowdimlem3  27190  axlowdimlem13  27200  axlowdimlem16  27203  axlowdimlem17  27204  2wlkdlem1  28166  elwwlks2s3  28192  elwspths2spth  28208  upgr3v3e3cycl  28420  upgr4cycl4dv4e  28425  konigsberglem5  28496  ipval2  28945  stm1add3i  30485  stadd3i  30486  problem2  33499  problem4  33501  sinccvglem  33505  mblfinlem3  35722  heiborlem6  35880  aks4d1p1  39990  2ap1caineq  40001  fac2xp3  40060  sn-0ne2  40282  3cubeslem2  40395  3cubeslem3r  40397  rmydioph  40724  rmxdioph  40726  expdiophlem2  40732  expdioph  40733  amgm3d  41672  stoweidlem26  43430  31prm  44910  lighneallem4b  44922  3odd  45021  sbgoldbo  45100  itcoval3  45872  ackval3  45890