Theorem 2timesd 9228

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

Hypothesis

Ref	Expression
2timesd.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
2timesd	|- ( ph -> ( 2 x. A ) = ( A + A ) )

Proof of Theorem 2timesd

Step	Hyp	Ref	Expression
1		2timesd.1	. 2 |- ( ph -> A e. CC )
2		2times 9112	. 2 |- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
3	1, 2	syl 14	1 |- ( ph -> ( 2 x. A ) = ( A + A ) )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5919   CCcc 7872   + caddc 7877   x. cmul 7879   2c2 9035

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966  ax-1cn 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-mulcom 7975  ax-mulass 7977  ax-distr 7978  ax-1rid 7981  ax-cnre 7985

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-2 9043

This theorem is referenced by:  xleaddadd  9956  fzctr  10202  flhalf  10374  q2submod  10459  modaddmodup  10461  m1expeven  10660  binom2  10725  nn0opthlem2d  10795  crre  11004  imval2  11041  resqrexlemdec  11158  amgm2  11265  maxabsle  11351  maxabslemab  11353  maxltsup  11365  max0addsup  11366  arisum2  11645  efival  11878  sinadd  11882  cosadd  11883  addsin  11888  subsin  11889  cosmul  11891  addcos  11892  subcos  11893  sin2t  11895  cos2t  11896  eirraplem  11923  pythagtriplem12  12416  pythagtriplem15  12419  pythagtriplem17  12421  difsqpwdvds  12479  4sqlem11  12542  4sqlem12  12543  bl2in  14582  cosordlem  15025  gausslemma2d  15226  lgsquadlem1  15234  apdifflemf  15606  apdifflemr  15607