Theorem 2timesi 12354

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 12352	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Syntax hints:   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   + caddc 11115   · cmul 11117  2c2 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-2 12279

This theorem is referenced by:  2t2e4  12380  nn0le2xi  12530  binom2i  14180  rddif  15291  abs3lemi  15361  iseraltlem2  15633  prmreclem6  16858  mod2xi  17006  numexp2x  17016  prmlem2  17057  iihalf2  24675  pcoass  24771  ovolunlem1a  25245  tangtx  26251  sinq34lt0t  26255  eff1o  26294  ang180lem2  26551  dvatan  26676  basellem2  26822  basellem5  26825  chtub  26951  bposlem9  27031  ex-dvds  29976  norm3lem  30669  normpari  30674  polid2i  30677  ballotth  33834  heiborlem6  36987  sqsumi  41495  dirkertrigeqlem1  45112  fourierdlem94  45214  fourierdlem102  45222  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  fourierdlem114  45234  sqwvfoura  45242  sqwvfourb  45243  fouriersw  45245  fmtnorec3  46514  2t6m3t4e0  47112  zlmodzxzequa  47264