Theorem 2timesd 9095

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 8981	. 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 1343   e. wcel 2136  (class class class)co 5841   CCcc 7747   + caddc 7752   x. cmul 7754   2c2 8904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841  ax-1cn 7842  ax-icn 7844  ax-addcl 7845  ax-mulcl 7847  ax-mulcom 7850  ax-mulass 7852  ax-distr 7853  ax-1rid 7856  ax-cnre 7860

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-2 8912

This theorem is referenced by:  xleaddadd  9819  fzctr  10064  flhalf  10233  q2submod  10316  modaddmodup  10318  m1expeven  10498  binom2  10562  nn0opthlem2d  10630  crre  10795  imval2  10832  resqrexlemdec  10949  amgm2  11056  maxabsle  11142  maxabslemab  11144  maxltsup  11156  max0addsup  11157  arisum2  11436  efival  11669  sinadd  11673  cosadd  11674  addsin  11679  subsin  11680  cosmul  11682  addcos  11683  subcos  11684  sin2t  11686  cos2t  11687  eirraplem  11713  pythagtriplem12  12203  pythagtriplem15  12206  pythagtriplem17  12208  difsqpwdvds  12265  bl2in  13003  cosordlem  13370  apdifflemf  13885  apdifflemr  13886