Theorem 2timesd 9225

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 9110	. 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 5918   CCcc 7870   + caddc 7875   x. cmul 7877   2c2 9033

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 7964  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-mulcom 7973  ax-mulass 7975  ax-distr 7976  ax-1rid 7979  ax-cnre 7983

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 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-2 9041

This theorem is referenced by:  xleaddadd  9953  fzctr  10199  flhalf  10371  q2submod  10456  modaddmodup  10458  m1expeven  10657  binom2  10722  nn0opthlem2d  10792  crre  11001  imval2  11038  resqrexlemdec  11155  amgm2  11262  maxabsle  11348  maxabslemab  11350  maxltsup  11362  max0addsup  11363  arisum2  11642  efival  11875  sinadd  11879  cosadd  11880  addsin  11885  subsin  11886  cosmul  11888  addcos  11889  subcos  11890  sin2t  11892  cos2t  11893  eirraplem  11920  pythagtriplem12  12413  pythagtriplem15  12416  pythagtriplem17  12418  difsqpwdvds  12476  4sqlem11  12539  4sqlem12  12540  bl2in  14571  cosordlem  14984  gausslemma2d  15185  lgsquadlem1  15191  apdifflemf  15536  apdifflemr  15537