Theorem 2timesi 12355

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071   + caddc 11076   · cmul 11078  2c2 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-mulcom 11137  ax-mulass 11139  ax-distr 11140  ax-1rid 11143  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280

This theorem is referenced by:  2t2e4  12381  binom2i  14225  rddif  15368  abs3lemi  15438  iseraltlem2  15710  prmreclem6  16957  mod2xi  17105  numexp2x  17114  prmlem2  17156  iihalf2  24995  pcoass  25086  ovolunlem1a  25558  tangtx  26570  sinq34lt0t  26574  eff1o  26614  ang180lem2  26875  dvatan  27000  basellem2  27146  basellem5  27149  chtub  27276  bposlem9  27356  ex-dvds  30658  norm3lem  31352  normpari  31357  polid2i  31360  ballotth  34835  heiborlem6  38315  sqsumi  42890  dirkertrigeqlem1  46672  fourierdlem94  46774  fourierdlem102  46782  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  fourierdlem114  46794  sqwvfoura  46802  sqwvfourb  46803  fouriersw  46805  sin5tlem1  47467  fmtnorec3  48157  2t6m3t4e0  48970  zlmodzxzequa  49118