Theorem adddid 10992

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddid	⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddi 10953	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  (class class class)co 7269  ℂcc 10862   + caddc 10867   · cmul 10869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 10931

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  addid1  11147  cnegex  11148  addcom  11153  addcomd  11169  subdi  11400  conjmul  11684  cju  11961  flhalf  13540  modcyc  13616  addmodlteq  13656  binom3  13929  sqoddm1div8  13948  bcpasc  14025  hashf1lem2  14160  remim  14818  mulre  14822  readd  14827  remullem  14829  imadd  14835  cjadd  14842  sqreulem  15061  iseraltlem2  15384  o1fsum  15515  binomlem  15531  climcndslem2  15552  binomfallfaclem2  15740  bpoly4  15759  tanval3  15833  sinadd  15863  tanadd  15866  dvdsmulgcd  16255  lcmgcdlem  16301  pythagtriplem1  16507  pcaddlem  16579  prmreclem4  16610  prmreclem6  16612  mul4sqlem  16644  vdwlem3  16674  vdwlem6  16677  vdwlem9  16680  nn0srg  20658  rge0srg  20659  mhppwdeg  21330  icopnfcnv  24095  pcoass  24177  cphipval2  24395  minveclem2  24580  pjthlem1  24591  ovolunlem1a  24650  ovolscalem1  24667  itgcnlem  24944  itgadd  24979  itgmulc2  24988  itgsplit  24990  aaliou3lem2  25493  abelthlem7  25587  tangtx  25652  efgh  25687  tanarg  25764  logcnlem4  25790  mulcxp  25830  cxpmul2  25834  heron  25978  quad2  25979  dcubic1lem  25983  dcubic2  25984  mcubic  25987  binom4  25990  quart1  25996  atanlogsublem  26055  2efiatan  26058  lgamgulmlem3  26170  basellem2  26221  basellem3  26222  basellem8  26227  chtub  26350  bposlem9  26430  lgseisenlem2  26514  2lgsoddprmlem2  26547  2sqlem4  26559  2sqlem8  26564  dchrisumlem1  26627  dchrvmasum2if  26635  dchrisum0re  26651  mulog2sumlem1  26672  selberglem1  26683  selberglem2  26684  selberg  26686  selberg2  26689  chpdifbndlem1  26691  selberg3lem1  26695  selberg4  26699  pntsval2  26714  pntibndlem2  26729  pntlemr  26740  pntlemf  26743  pntlemo  26745  ostth2lem2  26772  ostth2lem3  26773  brbtwn2  27263  axsegconlem9  27283  axpasch  27299  axeuclidlem  27320  axcontlem2  27323  axcontlem4  27325  axcontlem7  27328  axcontlem8  27329  finsumvtxdg2ssteplem4  27905  ipasslem2  29182  minvecolem2  29225  pjhthlem1  29741  wrdt2ind  31213  ccfldsrarelvec  31729  circlemeth  32608  subfacval2  33137  subfaclim  33138  faclimlem1  33697  itgaddnc  35825  itgmulc2nc  35833  dvasin  35849  2np3bcnp1  40089  nnadddir  40289  nnmul1com  40290  nnmulcom  40291  resubdi  40368  sn-negex12  40387  sn-mul01  40396  sn-mulid2  40406  sn-0tie0  40410  sn-mul02  40411  cnreeu  40427  fltmul  40461  cu3addd  40491  3cubeslem3l  40497  3cubeslem3r  40498  pellexlem6  40645  pell1234qrmulcl  40666  rmxyadd  40732  jm2.25  40810  relexpmulnn  41279  binomcxplemnotnn0  41936  sumnnodd  43134  dvnmul  43447  stoweidlem13  43517  wallispilem4  43572  wallispi2lem1  43575  wallispi2lem2  43576  stirlinglem1  43578  stirlinglem6  43583  stirlinglem7  43584  stirlinglem8  43585  stirlinglem10  43587  dirkerper  43600  dirkertrigeqlem1  43602  dirkertrigeqlem2  43603  dirkertrigeqlem3  43604  fourierdlem83  43693  hoidmvlelem2  44097  hspmbllem1  44127  smfmullem1  44285  deccarry  44764  fmtnorec4  44962  mod42tp1mod8  45015  lighneallem3  45020  opoeALTV  45096  opeoALTV  45097  2zlidl  45453  2zrngamgm  45458  altgsumbcALT  45650  itcovalpclem2  45978  ackval2  45989  affinecomb2  46010  itscnhlc0yqe  46066  itsclc0yqsollem1  46069  itsclc0yqsol  46071  itscnhlc0xyqsol  46072  itsclc0xyqsolr  46076  itscnhlinecirc02plem1  46089