Theorem 2timesi 11778

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   + caddc 10542   · cmul 10544  2c2 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703

This theorem is referenced by:  2t2e4  11804  nn0le2xi  11954  binom2i  13577  rddif  14702  abs3lemi  14772  iseraltlem2  15041  prmreclem6  16259  mod2xi  16407  numexp2x  16417  prmlem2  16455  iihalf2  23539  pcoass  23630  ovolunlem1a  24099  tangtx  25093  sinq34lt0t  25097  eff1o  25135  ang180lem2  25390  dvatan  25515  basellem2  25661  basellem5  25664  chtub  25790  bposlem9  25870  ex-dvds  28237  norm3lem  28928  normpari  28933  polid2i  28936  ballotth  31797  heiborlem6  35096  sqsumi  39174  dirkertrigeqlem1  42390  fourierdlem94  42492  fourierdlem102  42500  fourierdlem111  42509  fourierdlem112  42510  fourierdlem113  42511  fourierdlem114  42512  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  fmtnorec3  43717  2t6m3t4e0  44403  zlmodzxzequa  44558