Theorem 2timesi 12378

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098   + caddc 11103   · cmul 11105  2c2 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303

This theorem is referenced by:  2t2e4  12404  binom2i  14248  rddif  15392  abs3lemi  15462  iseraltlem2  15734  prmreclem6  16981  mod2xi  17129  numexp2x  17138  prmlem2  17180  iihalf2  25061  pcoass  25152  ovolunlem1a  25624  tangtx  26636  sinq34lt0t  26640  eff1o  26680  ang180lem2  26941  dvatan  27066  basellem2  27212  basellem5  27215  chtub  27342  bposlem9  27422  ex-dvds  30748  norm3lem  31442  normpari  31447  polid2i  31450  ballotth  34873  heiborlem6  38355  sqsumi  42932  dirkertrigeqlem1  46704  fourierdlem94  46806  fourierdlem102  46814  fourierdlem111  46823  fourierdlem112  46824  fourierdlem113  46825  fourierdlem114  46826  sqwvfoura  46834  sqwvfourb  46835  fouriersw  46837  sin5tlem1  47499  fmtnorec3  48189  2t6m3t4e0  49013  zlmodzxzequa  49161