Theorem 2timesd 9429

Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
2timesd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
2timesd	⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Proof of Theorem 2timesd

Step	Hyp	Ref	Expression
1		2timesd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		2times 9313	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078   · cmul 8080  2c2 9236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-resscn 8167  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-mulcom 8176  ax-mulass 8178  ax-distr 8179  ax-1rid 8182  ax-cnre 8186

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-2 9244

This theorem is referenced by:  xleaddadd  10166  fzctr  10413  flhalf  10608  q2submod  10693  modaddmodup  10695  m1expeven  10894  binom2  10959  nn0opthlem2d  11029  crre  11480  imval2  11517  resqrexlemdec  11634  amgm2  11741  maxabsle  11827  maxabslemab  11829  maxltsup  11841  max0addsup  11842  arisum2  12123  efival  12356  sinadd  12360  cosadd  12361  addsin  12366  subsin  12367  cosmul  12369  addcos  12370  subcos  12371  sin2t  12373  cos2t  12374  eirraplem  12401  pythagtriplem12  12911  pythagtriplem15  12914  pythagtriplem17  12916  difsqpwdvds  12974  4sqlem11  13037  4sqlem12  13038  bl2in  15197  cosordlem  15643  gausslemma2d  15871  lgsquadlem1  15879  apdifflemf  16761  apdifflemr  16762