Theorem 2timesi 12341

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

Syntax hints:   = wceq 1550   ∈ wcel 2132  (class class class)co 7381  ℂcc 11057   + caddc 11062   · cmul 11064  2c2 12258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-mulcl 11121  ax-mulcom 11123  ax-mulass 11125  ax-distr 11126  ax-1rid 11129  ax-cnre 11132

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-2 12266

This theorem is referenced by:  2t2e4  12367  binom2i  14211  rddif  15340  abs3lemi  15410  iseraltlem2  15682  prmreclem6  16929  mod2xi  17077  numexp2x  17086  prmlem2  17128  iihalf2  24964  pcoass  25055  ovolunlem1a  25527  tangtx  26536  sinq34lt0t  26540  eff1o  26580  ang180lem2  26841  dvatan  26966  basellem2  27112  basellem5  27115  chtub  27242  bposlem9  27322  ex-dvds  30593  norm3lem  31287  normpari  31292  polid2i  31295  ballotth  34779  heiborlem6  38253  sqsumi  42828  dirkertrigeqlem1  46610  fourierdlem94  46712  fourierdlem102  46720  fourierdlem111  46729  fourierdlem112  46730  fourierdlem113  46731  fourierdlem114  46732  sqwvfoura  46740  sqwvfourb  46741  fouriersw  46743  sin5tlem1  47405  fmtnorec3  48095  2t6m3t4e0  48908  zlmodzxzequa  49056