Theorem adddid 11221

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   · cmul 11093

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

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

This theorem is referenced by:  addrid  11378  cnegex  11379  addcom  11384  addcomd  11400  subdi  11635  conjmul  11920  cju  12202  nnadddir  12280  nnmul1com  12281  nnmulcom  12282  flhalf  13851  modcyc  13927  addmodlteq  13970  binom3  14248  sqoddm1div8  14267  bcpasc  14345  hashf1lem2  14481  remim  15156  mulre  15160  readd  15165  remullem  15167  imadd  15173  cjadd  15180  sqreulem  15399  iseraltlem2  15722  o1fsum  15853  binomlem  15871  climcndslem2  15892  binomfallfaclem2  16082  bpoly4  16101  tanval3  16178  sinadd  16208  tanadd  16211  dvdsmulgcd  16602  lcmgcdlem  16652  pythagtriplem1  16864  pcaddlem  16936  prmreclem4  16967  prmreclem6  16969  mul4sqlem  17001  vdwlem3  17031  vdwlem6  17034  vdwlem9  17037  nn0srg  21544  rge0srg  21545  mhppwdeg  22270  icopnfcnv  25058  pcoass  25140  cphipval2  25357  minveclem2  25542  pjthlem1  25553  ovolunlem1a  25612  ovolscalem1  25629  itgcnlem  25906  itgadd  25941  itgmulc2  25950  itgsplit  25952  aaliou3lem2  26461  abelthlem7  26555  tangtx  26624  efgh  26660  tanarg  26738  logcnlem4  26764  mulcxp  26804  cxpmul2  26808  heron  26957  quad2  26958  dcubic1lem  26962  dcubic2  26963  mcubic  26966  binom4  26969  quart1  26975  atanlogsublem  27034  2efiatan  27037  lgamgulmlem3  27149  basellem2  27200  basellem3  27201  basellem8  27206  chtub  27330  bposlem9  27410  lgseisenlem2  27494  2lgsoddprmlem2  27527  2sqlem4  27539  2sqlem8  27544  dchrisumlem1  27607  dchrvmasum2if  27615  dchrisum0re  27631  mulog2sumlem1  27652  selberglem1  27663  selberglem2  27664  selberg  27666  selberg2  27669  chpdifbndlem1  27671  selberg3lem1  27675  selberg4  27679  pntsval2  27694  pntibndlem2  27709  pntlemr  27720  pntlemf  27723  pntlemo  27725  ostth2lem2  27752  ostth2lem3  27753  brbtwn2  29160  axsegconlem9  29180  axpasch  29196  axeuclidlem  29217  axcontlem2  29220  axcontlem4  29222  axcontlem7  29225  axcontlem8  29226  finsumvtxdg2ssteplem4  29803  ipasslem2  31089  minvecolem2  31132  pjhthlem1  31648  wrdt2ind  33181  ccfldsrarelvec  33973  constrrtcclem  34036  constrremulcl  34069  constrrecl  34071  circlemeth  34939  subfacval2  35545  subfaclim  35546  faclimlem1  36101  itgaddnc  38186  itgmulc2nc  38194  dvasin  38210  posbezout  42724  2np3bcnp1  42768  sumcubes  42929  resubdi  43012  sn-negex12  43033  sn-mul01  43042  sn-mullid  43052  redivdird  43078  sn-0tie0  43080  sn-mul02  43081  renegmulnnass  43094  cnreeu  43119  fltmul  43224  cu3addd  43269  3cubeslem3l  43274  3cubeslem3r  43275  pellexlem6  43418  pell1234qrmulcl  43439  rmxyadd  43505  jm2.25  43583  relexpmulnn  44292  binomcxplemnotnn0  44925  sumnnodd  46205  dvnmul  46516  stoweidlem13  46586  wallispilem4  46641  wallispi2lem1  46644  wallispi2lem2  46645  stirlinglem1  46647  stirlinglem6  46652  stirlinglem7  46653  stirlinglem8  46654  stirlinglem10  46656  dirkerper  46669  dirkertrigeqlem1  46671  dirkertrigeqlem2  46672  dirkertrigeqlem3  46673  fourierdlem83  46762  hoidmvlelem2  47169  hspmbllem1  47199  smfmullem1  47364  sin5tlem4  47469  deccarry  47904  fmtnorec4  48157  mod42tp1mod8  48210  lighneallem3  48215  opoeALTV  48304  opeoALTV  48305  2zlidl  48861  2zrngamgm  48866  altgsumbcALT  48985  itcovalpclem2  49303  ackval2  49314  affinecomb2  49335  itscnhlc0yqe  49391  itsclc0yqsollem1  49394  itsclc0yqsol  49396  itscnhlc0xyqsol  49397  itsclc0xyqsolr  49401  itscnhlinecirc02plem1  49414