Theorem adddid 11234

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 11190	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104   · cmul 11106

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  addrid  11391  cnegex  11392  addcom  11397  addcomd  11413  subdi  11648  conjmul  11933  cju  12215  nnadddir  12293  nnmul1com  12294  nnmulcom  12295  flhalf  13865  modcyc  13941  addmodlteq  13984  binom3  14262  sqoddm1div8  14281  bcpasc  14359  hashf1lem2  14495  remim  15170  mulre  15174  readd  15179  remullem  15181  imadd  15187  cjadd  15194  sqreulem  15413  iseraltlem2  15736  o1fsum  15867  binomlem  15885  climcndslem2  15906  binomfallfaclem2  16095  bpoly4  16114  tanval3  16191  sinadd  16221  tanadd  16224  dvdsmulgcd  16615  lcmgcdlem  16665  pythagtriplem1  16877  pcaddlem  16949  prmreclem4  16980  prmreclem6  16982  mul4sqlem  17014  vdwlem3  17044  vdwlem6  17047  vdwlem9  17050  nn0srg  21568  rge0srg  21569  mhppwdeg  22294  icopnfcnv  25082  pcoass  25164  cphipval2  25381  minveclem2  25566  pjthlem1  25577  ovolunlem1a  25636  ovolscalem1  25653  itgcnlem  25930  itgadd  25965  itgmulc2  25974  itgsplit  25976  aaliou3lem2  26487  abelthlem7  26582  tangtx  26651  efgh  26687  tanarg  26765  logcnlem4  26791  mulcxp  26831  cxpmul2  26835  heron  26984  quad2  26985  dcubic1lem  26989  dcubic2  26990  mcubic  26993  binom4  26996  quart1  27002  atanlogsublem  27061  2efiatan  27064  lgamgulmlem3  27176  basellem2  27227  basellem3  27228  basellem8  27233  chtub  27357  bposlem9  27437  lgseisenlem2  27521  2lgsoddprmlem2  27554  2sqlem4  27566  2sqlem8  27571  dchrisumlem1  27634  dchrvmasum2if  27642  dchrisum0re  27658  mulog2sumlem1  27679  selberglem1  27690  selberglem2  27691  selberg  27693  selberg2  27696  chpdifbndlem1  27698  selberg3lem1  27702  selberg4  27706  pntsval2  27721  pntibndlem2  27736  pntlemr  27747  pntlemf  27750  pntlemo  27752  ostth2lem2  27779  ostth2lem3  27780  brbtwn2  29236  axsegconlem9  29256  axpasch  29272  axeuclidlem  29293  axcontlem2  29296  axcontlem4  29298  axcontlem7  29301  axcontlem8  29302  finsumvtxdg2ssteplem4  29879  ipasslem2  31165  minvecolem2  31208  pjhthlem1  31724  wrdt2ind  33254  ccfldsrarelvec  34042  constrrtcclem  34105  constrremulcl  34138  constrrecl  34140  circlemeth  35008  subfacval2  35660  subfaclim  35661  faclimlem1  36216  itgaddnc  38312  itgmulc2nc  38320  dvasin  38336  posbezout  42848  2np3bcnp1  42892  quadfac  42953  sumcubes  43055  resubdi  43138  sn-negex12  43159  sn-mul01  43168  sn-mullid  43178  redivdird  43204  sn-0tie0  43206  sn-mul02  43207  renegmulnnass  43220  cnreeu  43245  fltmul  43350  cu3addd  43395  3cubeslem3l  43400  3cubeslem3r  43401  pellexlem6  43544  pell1234qrmulcl  43565  rmxyadd  43631  jm2.25  43709  relexpmulnn  44418  binomcxplemnotnn0  45049  sumnnodd  46329  dvnmul  46640  stoweidlem13  46710  wallispilem4  46765  wallispi2lem1  46768  wallispi2lem2  46769  stirlinglem1  46771  stirlinglem6  46776  stirlinglem7  46777  stirlinglem8  46778  stirlinglem10  46780  dirkerper  46793  dirkertrigeqlem1  46795  dirkertrigeqlem2  46796  dirkertrigeqlem3  46797  fourierdlem83  46886  hoidmvlelem2  47293  hspmbllem1  47323  smfmullem1  47488  sin5tlem4  47596  deccarry  48031  fmtnorec4  48284  mod42tp1mod8  48337  lighneallem3  48342  opoeALTV  48431  opeoALTV  48432  2zlidl  48988  2zrngamgm  48993  altgsumbcALT  49116  itcovalpclem2  49434  ackval2  49445  affinecomb2  49466  itscnhlc0yqe  49522  itsclc0yqsollem1  49525  itsclc0yqsol  49527  itscnhlc0xyqsol  49528  itsclc0xyqsolr  49532  itscnhlinecirc02plem1  49545