Theorem 2timesi 12383

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137   · cmul 11139  2c2 12300

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 2708  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-mulcl 11196  ax-mulcom 11198  ax-mulass 11200  ax-distr 11201  ax-1rid 11204  ax-cnre 11207

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 2715  df-cleq 2728  df-clel 2810  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308

This theorem is referenced by:  2t2e4  12409  binom2i  14235  rddif  15364  abs3lemi  15434  iseraltlem2  15704  prmreclem6  16946  mod2xi  17094  numexp2x  17103  prmlem2  17144  iihalf2  24884  pcoass  24980  ovolunlem1a  25454  tangtx  26471  sinq34lt0t  26475  eff1o  26515  ang180lem2  26777  dvatan  26902  basellem2  27049  basellem5  27052  chtub  27180  bposlem9  27260  ex-dvds  30442  norm3lem  31135  normpari  31140  polid2i  31143  ballotth  34575  heiborlem6  37845  sqsumi  42298  dirkertrigeqlem1  46094  fourierdlem94  46196  fourierdlem102  46204  fourierdlem111  46213  fourierdlem112  46214  fourierdlem113  46215  fourierdlem114  46216  sqwvfoura  46224  sqwvfourb  46225  fouriersw  46227  fmtnorec3  47529  2t6m3t4e0  48290  zlmodzxzequa  48439