Theorem 2timesi 12326

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   · cmul 11080  2c2 12248

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 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256

This theorem is referenced by:  2t2e4  12352  binom2i  14184  rddif  15314  abs3lemi  15384  iseraltlem2  15656  prmreclem6  16899  mod2xi  17047  numexp2x  17056  prmlem2  17097  iihalf2  24835  pcoass  24931  ovolunlem1a  25404  tangtx  26421  sinq34lt0t  26425  eff1o  26465  ang180lem2  26727  dvatan  26852  basellem2  26999  basellem5  27002  chtub  27130  bposlem9  27210  ex-dvds  30392  norm3lem  31085  normpari  31090  polid2i  31093  ballotth  34536  heiborlem6  37817  sqsumi  42276  dirkertrigeqlem1  46103  fourierdlem94  46205  fourierdlem102  46213  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  fmtnorec3  47553  2t6m3t4e0  48340  zlmodzxzequa  48489