Theorem 2timesi 12373

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098   · cmul 11100  2c2 12290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298

This theorem is referenced by:  2t2e4  12399  binom2i  14244  rddif  15388  abs3lemi  15458  iseraltlem2  15730  prmreclem6  16976  mod2xi  17124  numexp2x  17133  prmlem2  17175  iihalf2  25092  pcoass  25183  ovolunlem1a  25655  tangtx  26670  sinq34lt0t  26674  eff1o  26714  ang180lem2  26975  dvatan  27100  basellem2  27246  basellem5  27249  chtub  27376  bposlem9  27456  ex-dvds  30807  norm3lem  31501  normpari  31506  polid2i  31509  ballotth  34928  heiborlem6  38487  sqsumi  43062  dirkertrigeqlem1  46832  fourierdlem94  46934  fourierdlem102  46942  fourierdlem111  46951  fourierdlem112  46952  fourierdlem113  46953  fourierdlem114  46954  sqwvfoura  46962  sqwvfourb  46963  fouriersw  46965  sin5tlem1  47630  fmtnorec3  48320  2t6m3t4e0  49148  zlmodzxzequa  49296