Theorem 2timesd 9161

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 9047	. 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 1353   e. wcel 2148  (class class class)co 5875   CCcc 7809   + caddc 7814   x. cmul 7816   2c2 8970

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-mulcom 7912  ax-mulass 7914  ax-distr 7915  ax-1rid 7918  ax-cnre 7922

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-2 8978

This theorem is referenced by:  xleaddadd  9887  fzctr  10133  flhalf  10302  q2submod  10385  modaddmodup  10387  m1expeven  10567  binom2  10632  nn0opthlem2d  10701  crre  10866  imval2  10903  resqrexlemdec  11020  amgm2  11127  maxabsle  11213  maxabslemab  11215  maxltsup  11227  max0addsup  11228  arisum2  11507  efival  11740  sinadd  11744  cosadd  11745  addsin  11750  subsin  11751  cosmul  11753  addcos  11754  subcos  11755  sin2t  11757  cos2t  11758  eirraplem  11784  pythagtriplem12  12275  pythagtriplem15  12278  pythagtriplem17  12280  difsqpwdvds  12337  bl2in  13906  cosordlem  14273  apdifflemf  14797  apdifflemr  14798