Theorem adddid 11156

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11313  cnegex  11314  addcom  11319  addcomd  11335  subdi  11570  conjmul  11858  cju  12141  flhalf  13750  modcyc  13826  addmodlteq  13869  binom3  14147  sqoddm1div8  14166  bcpasc  14244  hashf1lem2  14379  remim  15040  mulre  15044  readd  15049  remullem  15051  imadd  15057  cjadd  15064  sqreulem  15283  iseraltlem2  15606  o1fsum  15736  binomlem  15752  climcndslem2  15773  binomfallfaclem2  15963  bpoly4  15982  tanval3  16059  sinadd  16089  tanadd  16092  dvdsmulgcd  16483  lcmgcdlem  16533  pythagtriplem1  16744  pcaddlem  16816  prmreclem4  16847  prmreclem6  16849  mul4sqlem  16881  vdwlem3  16911  vdwlem6  16914  vdwlem9  16917  nn0srg  21392  rge0srg  21393  mhppwdeg  22093  icopnfcnv  24896  pcoass  24980  cphipval2  25197  minveclem2  25382  pjthlem1  25393  ovolunlem1a  25453  ovolscalem1  25470  itgcnlem  25747  itgadd  25782  itgmulc2  25791  itgsplit  25793  aaliou3lem2  26307  abelthlem7  26404  tangtx  26470  efgh  26506  tanarg  26584  logcnlem4  26610  mulcxp  26650  cxpmul2  26654  heron  26804  quad2  26805  dcubic1lem  26809  dcubic2  26810  mcubic  26813  binom4  26816  quart1  26822  atanlogsublem  26881  2efiatan  26884  lgamgulmlem3  26997  basellem2  27048  basellem3  27049  basellem8  27054  chtub  27179  bposlem9  27259  lgseisenlem2  27343  2lgsoddprmlem2  27376  2sqlem4  27388  2sqlem8  27393  dchrisumlem1  27456  dchrvmasum2if  27464  dchrisum0re  27480  mulog2sumlem1  27501  selberglem1  27512  selberglem2  27513  selberg  27515  selberg2  27518  chpdifbndlem1  27520  selberg3lem1  27524  selberg4  27528  pntsval2  27543  pntibndlem2  27558  pntlemr  27569  pntlemf  27572  pntlemo  27574  ostth2lem2  27601  ostth2lem3  27602  brbtwn2  28978  axsegconlem9  28998  axpasch  29014  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  finsumvtxdg2ssteplem4  29622  ipasslem2  30907  minvecolem2  30950  pjhthlem1  31466  wrdt2ind  33035  ccfldsrarelvec  33828  constrrtcclem  33891  constrremulcl  33924  constrrecl  33926  circlemeth  34797  subfacval2  35381  subfaclim  35382  faclimlem1  35937  itgaddnc  37881  itgmulc2nc  37889  dvasin  37905  posbezout  42354  2np3bcnp1  42398  nnadddir  42525  nnmul1com  42526  nnmulcom  42527  sumcubes  42568  resubdi  42651  sn-negex12  42672  sn-mul01  42681  sn-mullid  42691  sn-0tie0  42706  sn-mul02  42707  renegmulnnass  42720  cnreeu  42745  fltmul  42878  cu3addd  42923  3cubeslem3l  42928  3cubeslem3r  42929  pellexlem6  43076  pell1234qrmulcl  43097  rmxyadd  43163  jm2.25  43241  relexpmulnn  43950  binomcxplemnotnn0  44597  sumnnodd  45876  dvnmul  46187  stoweidlem13  46257  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  stirlinglem1  46318  stirlinglem6  46323  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  dirkerper  46340  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  fourierdlem83  46433  hoidmvlelem2  46840  hspmbllem1  46870  smfmullem1  47035  deccarry  47557  fmtnorec4  47795  mod42tp1mod8  47848  lighneallem3  47853  opoeALTV  47929  opeoALTV  47930  2zlidl  48486  2zrngamgm  48491  altgsumbcALT  48599  itcovalpclem2  48917  ackval2  48928  affinecomb2  48949  itscnhlc0yqe  49005  itsclc0yqsollem1  49008  itsclc0yqsol  49010  itscnhlc0xyqsol  49011  itsclc0xyqsolr  49015  itscnhlinecirc02plem1  49028