Theorem 2timesi 10681

Description: Two times a number. (Contributed by NM, 1-Aug-1999.)

Hypothesis

Ref	Expression
2timesi.1

Assertion

Ref	Expression
2timesi

Proof of Theorem 2timesi

Step	Hyp	Ref	Expression
1		2timesi.1	. 2
2		2times 10679	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296  cc 9511  caddc 9516  cmul 9518  2c2 10610

This theorem is referenced by:  2t2e4  10710  nn0le2xi  10872  binom2i  12277  rddif  13173  abs3lemi  13242  iseraltlem2  13505  prmreclem6  14439  mod2xi  14555  numexp2x  14565  prmlem2  14605  iihalf2  21433  pcoass  21524  ovolunlem1a  21907  tangtx  22898  sinq34lt0t  22902  eff1o  22936  ang180lem2  23142  dvatan  23266  basellem2  23355  basellem5  23358  chtub  23487  bposlem9  23567  ex-dvds  25169  norm3lem  26066  normpari  26071  polid2i  26074  ballotth  28476  heiborlem6  30312  rmspecsqrtnq  30842  dirkertrigeqlem1  31880  fourierdlem94  31983  fourierdlem102  31991  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  2t6m3t4e0  32937  zlmodzxzequa  33097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619