HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-2 8671
Description: Define the number 2.
Assertion
Ref Expression
df-2

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 8662 . 2
2 c1 7909 . . 3
3 caddc 7911 . . 3
42, 2, 3co 5206 . 2
51, 4wceq 1526 1
Colors of variables: wff set class
This definition is referenced by:  2re 8680  2pos 8691  1p1e2 8702  2p2e4 8703  2timesi 8704  3p2e5 8716  4p2e6 8718  5p2e7 8721  6p2e8 8725  7p2e9 8728  8p2e10 8730  2nn 8737  1lt2 8746  halfpos 8799  nneo 8936  6p6e12 9006  7p5e12 9008  8p4e12 9012  9p2e11 9017  9p3e12 9018  eluz2b1 9120  fztp 9482  fzprval 9485  fztpval 9486  sqval 9724  fac2 9809  faclbnd4lem1 9821  bcp1m1 9846  hashpr 9880  iseralt 10329  binom11 10451  climcndslem1 10466  climcndslem2 10467  ege2le3 10524  ef4p 10545  efgt1p2 10546  eirrlem 10628  odd2np1lem 10729  isprm3 10831  prmind2 10833  opoe 10895  pockthlem 10970  pockthg 10971  prmunb 10979  prmreclem2 10982  4sqlem19 11028  vdwlem12 11057  decexp2 11108  abvtrivd 12377  ovolunlem1a 14418  ovolicc1 14438  vitalilem2 14527  itgcnlem 14707  dveflem 14862  coskpi 15324  ang180lem3 15430  tanatan 15563  cosatan 15565  atantayl2 15582  emcllem7 15623  basellem3 15641  basellem5 15643  basellem8 15646  ppi2 15695  ppi3 15696  cht2 15697  ppieq0 15701  ppiublem 15704  chtublem 15707  chtub 15708  bcp1ctr 15713  bclbnd 15714  bposlem1 15718  bposlem2 15719  bposlem6 15723  lgslem1 15730  lgsval2lem 15740  lgsdir2lem2 15758  lgsdir2lem3 15759  lgsdirprm 15763  lgseisen 15781  m1lgs 15790  ex-fl 15863  1p1e2apr1 15868  vc2 16157  ipval2 16330  ip2i 16456  hv2times 16691  pjthlem1 17022  ho2times 17451  stm1addi 17876  staddi 17877  stadd3i 17879  addltmulALT 18077  subfacp1lem1 18102  subfacp1lem5 18107  subfacp1lem6 18108  vdgr1d 18272  konigsberg 18292  axlowdimlem4 18971  axlowdimlem13 18980  bpoly1 19184  bpolydiflem 19187  intset 20491  pell14qrgapw 21442  rmydioph 21592  rmxdioph 21594  expdiophlem1 21599  expdiophlem2 21600  expdioph 21601
Copyright terms: Public domain