Theorem 2timesd 9058

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 8944	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128  (class class class)co 5818  ℂcc 7713   + caddc 7718   · cmul 7720  2c2 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7807  ax-1cn 7808  ax-icn 7810  ax-addcl 7811  ax-mulcl 7813  ax-mulcom 7816  ax-mulass 7818  ax-distr 7819  ax-1rid 7822  ax-cnre 7826

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-iota 5132  df-fv 5175  df-ov 5821  df-2 8875

This theorem is referenced by:  xleaddadd  9773  fzctr  10014  flhalf  10183  q2submod  10266  modaddmodup  10268  m1expeven  10448  binom2  10511  nn0opthlem2d  10577  crre  10739  imval2  10776  resqrexlemdec  10893  amgm2  11000  maxabsle  11086  maxabslemab  11088  maxltsup  11100  max0addsup  11101  arisum2  11378  efival  11611  sinadd  11615  cosadd  11616  addsin  11621  subsin  11622  cosmul  11624  addcos  11625  subcos  11626  sin2t  11628  cos2t  11629  eirraplem  11655  bl2in  12763  cosordlem  13130  apdifflemf  13580  apdifflemr  13581