Theorem 2timesi 12402

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   + caddc 11156   · cmul 11158  2c2 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-mulcom 11217  ax-mulass 11219  ax-distr 11220  ax-1rid 11223  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327

This theorem is referenced by:  2t2e4  12428  binom2i  14248  rddif  15376  abs3lemi  15446  iseraltlem2  15716  prmreclem6  16955  mod2xi  17103  numexp2x  17113  prmlem2  17154  iihalf2  24975  pcoass  25071  ovolunlem1a  25545  tangtx  26562  sinq34lt0t  26566  eff1o  26606  ang180lem2  26868  dvatan  26993  basellem2  27140  basellem5  27143  chtub  27271  bposlem9  27351  ex-dvds  30485  norm3lem  31178  normpari  31183  polid2i  31186  ballotth  34519  heiborlem6  37803  sqsumi  42295  dirkertrigeqlem1  46054  fourierdlem94  46156  fourierdlem102  46164  fourierdlem111  46173  fourierdlem112  46174  fourierdlem113  46175  fourierdlem114  46176  sqwvfoura  46184  sqwvfourb  46185  fouriersw  46187  fmtnorec3  47473  2t6m3t4e0  48193  zlmodzxzequa  48342