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 1533   ∈ wcel 2098  (class class class)co 7405  ℂ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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  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 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6489  df-fv 6545  df-ov 7408  df-2 12279

This theorem is referenced by:  2t2e4  12380  nn0le2xi  12530  binom2i  14181  rddif  15293  abs3lemi  15363  iseraltlem2  15635  prmreclem6  16863  mod2xi  17011  numexp2x  17021  prmlem2  17062  iihalf2  24810  pcoass  24906  ovolunlem1a  25380  tangtx  26395  sinq34lt0t  26399  eff1o  26438  ang180lem2  26697  dvatan  26822  basellem2  26969  basellem5  26972  chtub  27100  bposlem9  27180  ex-dvds  30218  norm3lem  30911  normpari  30916  polid2i  30919  ballotth  34066  heiborlem6  37197  sqsumi  41756  dirkertrigeqlem1  45391  fourierdlem94  45493  fourierdlem102  45501  fourierdlem111  45510  fourierdlem112  45511  fourierdlem113  45512  fourierdlem114  45513  sqwvfoura  45521  sqwvfourb  45522  fouriersw  45524  fmtnorec3  46793  2t6m3t4e0  47305  zlmodzxzequa  47457