Theorem 2timesi 12395

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115   + caddc 11120   · cmul 11122  2c2 12312

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-mulcom 11181  ax-mulass 11183  ax-distr 11184  ax-1rid 11187  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320

This theorem is used by:  2t2e4  12421  binom2i  14268  rddif  15418  abs3lemi  15488  iseraltlem2  15760  prmreclem6  17005  mod2xi  17153  numexp2x  17162  prmlem2  17204  iihalf2  25145  pcoass  25236  ovolunlem1a  25708  tangtx  26723  sinq34lt0t  26727  eff1o  26767  ang180lem2  27028  dvatan  27153  basellem2  27299  basellem5  27302  chtub  27429  bposlem9  27509  ex-dvds  30880  norm3lem  31574  normpari  31579  polid2i  31582  ballotth  34995  heiborlem6  38527  sqsumi  43102  dirkertrigeqlem1  46872  fourierdlem94  46974  fourierdlem102  46982  fourierdlem111  46991  fourierdlem112  46992  fourierdlem113  46993  fourierdlem114  46994  sqwvfoura  47002  sqwvfourb  47003  fouriersw  47005  sin5tlem1  47670  fmtnorec3  48360  2t6m3t4e0  49187  zlmodzxzequa  49335