Theorem 2timesi 12278

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

Hypothesis

Ref	Expression
2timesi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
2timesi	⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Proof of Theorem 2timesi

Step	Hyp	Ref	Expression
1		2timesi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		2times 12276	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-1rid 11096  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208

This theorem is referenced by:  2t2e4  12304  binom2i  14135  rddif  15264  abs3lemi  15334  iseraltlem2  15606  prmreclem6  16849  mod2xi  16997  numexp2x  17006  prmlem2  17047  iihalf2  24884  pcoass  24980  ovolunlem1a  25453  tangtx  26470  sinq34lt0t  26474  eff1o  26514  ang180lem2  26776  dvatan  26901  basellem2  27048  basellem5  27051  chtub  27179  bposlem9  27259  ex-dvds  30531  norm3lem  31224  normpari  31229  polid2i  31232  ballotth  34695  heiborlem6  38017  sqsumi  42546  dirkertrigeqlem1  46352  fourierdlem94  46454  fourierdlem102  46462  fourierdlem111  46471  fourierdlem112  46472  fourierdlem113  46473  fourierdlem114  46474  sqwvfoura  46482  sqwvfourb  46483  fouriersw  46485  fmtnorec3  47804  2t6m3t4e0  48604  zlmodzxzequa  48752