Theorem 2timesd 8756

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 8642	. 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 1296   e. wcel 1445  (class class class)co 5690   CCcc 7445   + caddc 7450   x. cmul 7452   2c2 8571

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-resscn 7534  ax-1cn 7535  ax-icn 7537  ax-addcl 7538  ax-mulcl 7540  ax-mulcom 7543  ax-mulass 7545  ax-distr 7546  ax-1rid 7549  ax-cnre 7553

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693  df-2 8579

This theorem is referenced by:  xleaddadd  9453  fzctr  9693  flhalf  9858  q2submod  9941  modaddmodup  9943  m1expeven  10117  binom2  10180  nn0opthlem2d  10244  crre  10406  imval2  10443  resqrexlemdec  10559  amgm2  10666  maxabsle  10752  maxabslemab  10754  maxltsup  10766  max0addsup  10767  arisum2  11042  efival  11172  sinadd  11176  cosadd  11177  addsin  11182  subsin  11183  cosmul  11185  addcos  11186  subcos  11187  sin2t  11189  cos2t  11190  eirraplem  11213  bl2in  12189