Theorem 2timesd 9300

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5957  ℂcc 7943   + caddc 7948   · cmul 7950  2c2 9107

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8037  ax-1cn 8038  ax-icn 8040  ax-addcl 8041  ax-mulcl 8043  ax-mulcom 8046  ax-mulass 8048  ax-distr 8049  ax-1rid 8052  ax-cnre 8056

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960  df-2 9115

This theorem is referenced by:  xleaddadd  10029  fzctr  10275  flhalf  10467  q2submod  10552  modaddmodup  10554  m1expeven  10753  binom2  10818  nn0opthlem2d  10888  crre  11243  imval2  11280  resqrexlemdec  11397  amgm2  11504  maxabsle  11590  maxabslemab  11592  maxltsup  11604  max0addsup  11605  arisum2  11885  efival  12118  sinadd  12122  cosadd  12123  addsin  12128  subsin  12129  cosmul  12131  addcos  12132  subcos  12133  sin2t  12135  cos2t  12136  eirraplem  12163  pythagtriplem12  12673  pythagtriplem15  12676  pythagtriplem17  12678  difsqpwdvds  12736  4sqlem11  12799  4sqlem12  12800  bl2in  14950  cosordlem  15396  gausslemma2d  15621  lgsquadlem1  15629  apdifflemf  16126  apdifflemr  16127