Theorem 2timesi 12308

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030   + caddc 11035   · cmul 11037  2c2 12230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238

This theorem is referenced by:  2t2e4  12334  binom2i  14168  rddif  15297  abs3lemi  15367  iseraltlem2  15639  prmreclem6  16886  mod2xi  17034  numexp2x  17043  prmlem2  17084  iihalf2  24913  pcoass  25004  ovolunlem1a  25476  tangtx  26485  sinq34lt0t  26489  eff1o  26529  ang180lem2  26790  dvatan  26915  basellem2  27062  basellem5  27065  chtub  27192  bposlem9  27272  ex-dvds  30544  norm3lem  31238  normpari  31243  polid2i  31246  ballotth  34701  heiborlem6  38154  sqsumi  42730  dirkertrigeqlem1  46547  fourierdlem94  46649  fourierdlem102  46657  fourierdlem111  46666  fourierdlem112  46667  fourierdlem113  46668  fourierdlem114  46669  sqwvfoura  46677  sqwvfourb  46678  fouriersw  46680  sin5tlem1  47340  fmtnorec3  48026  2t6m3t4e0  48839  zlmodzxzequa  48987