MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3 Structured version   Visualization version   GIF version

Definition df-3 11690
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
StepHypRef Expression
1 c3 11682 . 2 class 3
2 c2 11681 . . 3 class 2
3 c1 10527 . . 3 class 1
4 caddc 10529 . . 3 class +
52, 3, 4co 7145 . 2 class (2 + 1)
61, 5wceq 1528 1 wff 3 = (2 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  3nn  11705  3re  11706  3cn  11707  3pos  11731  3m1e2  11754  2p2e4  11761  2p1e3  11768  3p3e6  11778  4p3e7  11780  5p3e8  11783  6p3e9  11786  3t3e9  11793  2lt3  11798  7p3e10  12162  7p6e13  12165  8p3e11  12168  8p5e13  12170  9p3e12  12175  9p4e13  12176  4t3e12  12185  5t3e15  12188  6t3e18  12192  7t3e21  12197  8t3e24  12203  9t3e27  12210  nn01to3  12330  fztpval  12959  fz0to3un2pr  12999  fz0to4untppr  13000  fzo0to42pr  13114  fzo1to4tp  13115  cu2  13553  i3  13556  binom3  13575  fac3  13630  hashtpg  13833  sqrlem7  14598  bpoly2  15401  bpoly4  15403  fsumcube  15404  ege2le3  15433  ef4p  15456  cos1bnd  15530  oddprmge3  16034  prmgaplem3  16379  13prm  16439  23prm  16442  43prm  16445  83prm  16446  163prm  16448  lt6abl  18946  cphipval  23775  vitalilem4  24141  itgcnlem  24319  dveflem  24505  sincosq3sgn  25015  sincosq4sgn  25016  tangtx  25020  sincos6thpi  25030  ang180lem2  25315  mcubic  25352  cubic2  25353  binom4  25355  dquartlem2  25357  quart1  25361  quartlem1  25362  log2ublem3  25454  basellem5  25590  basellem8  25593  basellem9  25594  ppi3  25676  cht3  25678  ppiublem1  25706  ppiublem2  25707  ppiub  25708  chtub  25716  bclbnd  25784  bposlem2  25789  bposlem9  25796  lgsdir2lem3  25831  dchrvmasumiflem1  26005  mulog2sumlem2  26039  pntlemk  26110  pntlemo  26111  axlowdimlem3  26658  axlowdimlem13  26668  axlowdimlem16  26671  axlowdimlem17  26672  2wlkdlem1  27632  elwwlks2s3  27658  elwspths2spth  27674  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  konigsberglem5  27963  ipval2  28412  stm1add3i  29952  stadd3i  29953  problem2  32807  problem4  32809  sinccvglem  32813  mblfinlem3  34813  heiborlem6  34977  sn-0ne2  39116  3cubeslem2  39162  3cubeslem3r  39164  rmydioph  39491  rmxdioph  39493  expdiophlem2  39499  expdioph  39500  amgm3d  40433  stoweidlem26  42192  31prm  43607  lighneallem4b  43621  3odd  43720  sbgoldbo  43799
  Copyright terms: Public domain W3C validator