Theorem 2timesi 12319

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071   · cmul 11073  2c2 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249

This theorem is referenced by:  2t2e4  12345  binom2i  14177  rddif  15307  abs3lemi  15377  iseraltlem2  15649  prmreclem6  16892  mod2xi  17040  numexp2x  17049  prmlem2  17090  iihalf2  24828  pcoass  24924  ovolunlem1a  25397  tangtx  26414  sinq34lt0t  26418  eff1o  26458  ang180lem2  26720  dvatan  26845  basellem2  26992  basellem5  26995  chtub  27123  bposlem9  27203  ex-dvds  30385  norm3lem  31078  normpari  31083  polid2i  31086  ballotth  34529  heiborlem6  37810  sqsumi  42269  dirkertrigeqlem1  46096  fourierdlem94  46198  fourierdlem102  46206  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fouriersw  46229  fmtnorec3  47546  2t6m3t4e0  48333  zlmodzxzequa  48482