Theorem adddid 11314

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   · cmul 11189

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

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

This theorem is referenced by:  addrid  11470  cnegex  11471  addcom  11476  addcomd  11492  subdi  11723  conjmul  12011  cju  12289  flhalf  13881  modcyc  13957  addmodlteq  13997  binom3  14273  sqoddm1div8  14292  bcpasc  14370  hashf1lem2  14505  remim  15166  mulre  15170  readd  15175  remullem  15177  imadd  15183  cjadd  15190  sqreulem  15408  iseraltlem2  15731  o1fsum  15861  binomlem  15877  climcndslem2  15898  binomfallfaclem2  16088  bpoly4  16107  tanval3  16182  sinadd  16212  tanadd  16215  dvdsmulgcd  16603  lcmgcdlem  16653  pythagtriplem1  16863  pcaddlem  16935  prmreclem4  16966  prmreclem6  16968  mul4sqlem  17000  vdwlem3  17030  vdwlem6  17033  vdwlem9  17036  nn0srg  21478  rge0srg  21479  mhppwdeg  22177  icopnfcnv  24992  pcoass  25076  cphipval2  25294  minveclem2  25479  pjthlem1  25490  ovolunlem1a  25550  ovolscalem1  25567  itgcnlem  25845  itgadd  25880  itgmulc2  25889  itgsplit  25891  aaliou3lem2  26403  abelthlem7  26500  tangtx  26565  efgh  26601  tanarg  26679  logcnlem4  26705  mulcxp  26745  cxpmul2  26749  heron  26899  quad2  26900  dcubic1lem  26904  dcubic2  26905  mcubic  26908  binom4  26911  quart1  26917  atanlogsublem  26976  2efiatan  26979  lgamgulmlem3  27092  basellem2  27143  basellem3  27144  basellem8  27149  chtub  27274  bposlem9  27354  lgseisenlem2  27438  2lgsoddprmlem2  27471  2sqlem4  27483  2sqlem8  27488  dchrisumlem1  27551  dchrvmasum2if  27559  dchrisum0re  27575  mulog2sumlem1  27596  selberglem1  27607  selberglem2  27608  selberg  27610  selberg2  27613  chpdifbndlem1  27615  selberg3lem1  27619  selberg4  27623  pntsval2  27638  pntibndlem2  27653  pntlemr  27664  pntlemf  27667  pntlemo  27669  ostth2lem2  27696  ostth2lem3  27697  brbtwn2  28938  axsegconlem9  28958  axpasch  28974  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  finsumvtxdg2ssteplem4  29584  ipasslem2  30864  minvecolem2  30907  pjhthlem1  31423  wrdt2ind  32920  ccfldsrarelvec  33681  constrrtcclem  33725  circlemeth  34617  subfacval2  35155  subfaclim  35156  faclimlem1  35705  itgaddnc  37640  itgmulc2nc  37648  dvasin  37664  posbezout  42057  2np3bcnp1  42101  nnadddir  42259  nnmul1com  42260  nnmulcom  42261  sumcubes  42301  resubdi  42372  sn-negex12  42392  sn-mul01  42401  sn-mullid  42411  sn-0tie0  42415  sn-mul02  42416  renegmulnnass  42429  cnreeu  42446  fltmul  42590  cu3addd  42636  3cubeslem3l  42642  3cubeslem3r  42643  pellexlem6  42790  pell1234qrmulcl  42811  rmxyadd  42878  jm2.25  42956  relexpmulnn  43671  binomcxplemnotnn0  44325  sumnnodd  45551  dvnmul  45864  stoweidlem13  45934  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem1  45995  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  fourierdlem83  46110  hoidmvlelem2  46517  hspmbllem1  46547  smfmullem1  46712  deccarry  47226  fmtnorec4  47423  mod42tp1mod8  47476  lighneallem3  47481  opoeALTV  47557  opeoALTV  47558  2zlidl  47963  2zrngamgm  47968  altgsumbcALT  48078  itcovalpclem2  48405  ackval2  48416  affinecomb2  48437  itscnhlc0yqe  48493  itsclc0yqsollem1  48496  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itsclc0xyqsolr  48503  itscnhlinecirc02plem1  48516