Theorem adddid 11286

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   + caddc 11159   · cmul 11161

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

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

This theorem is referenced by:  addrid  11442  cnegex  11443  addcom  11448  addcomd  11464  subdi  11697  conjmul  11985  cju  12263  flhalf  13871  modcyc  13947  addmodlteq  13988  binom3  14264  sqoddm1div8  14283  bcpasc  14361  hashf1lem2  14496  remim  15157  mulre  15161  readd  15166  remullem  15168  imadd  15174  cjadd  15181  sqreulem  15399  iseraltlem2  15720  o1fsum  15850  binomlem  15866  climcndslem2  15887  binomfallfaclem2  16077  bpoly4  16096  tanval3  16171  sinadd  16201  tanadd  16204  dvdsmulgcd  16594  lcmgcdlem  16644  pythagtriplem1  16855  pcaddlem  16927  prmreclem4  16958  prmreclem6  16960  mul4sqlem  16992  vdwlem3  17022  vdwlem6  17025  vdwlem9  17028  nn0srg  21456  rge0srg  21457  mhppwdeg  22155  icopnfcnv  24974  pcoass  25058  cphipval2  25276  minveclem2  25461  pjthlem1  25472  ovolunlem1a  25532  ovolscalem1  25549  itgcnlem  25826  itgadd  25861  itgmulc2  25870  itgsplit  25872  aaliou3lem2  26386  abelthlem7  26483  tangtx  26548  efgh  26584  tanarg  26662  logcnlem4  26688  mulcxp  26728  cxpmul2  26732  heron  26882  quad2  26883  dcubic1lem  26887  dcubic2  26888  mcubic  26891  binom4  26894  quart1  26900  atanlogsublem  26959  2efiatan  26962  lgamgulmlem3  27075  basellem2  27126  basellem3  27127  basellem8  27132  chtub  27257  bposlem9  27337  lgseisenlem2  27421  2lgsoddprmlem2  27454  2sqlem4  27466  2sqlem8  27471  dchrisumlem1  27534  dchrvmasum2if  27542  dchrisum0re  27558  mulog2sumlem1  27579  selberglem1  27590  selberglem2  27591  selberg  27593  selberg2  27596  chpdifbndlem1  27598  selberg3lem1  27602  selberg4  27606  pntsval2  27621  pntibndlem2  27636  pntlemr  27647  pntlemf  27650  pntlemo  27652  ostth2lem2  27679  ostth2lem3  27680  brbtwn2  28921  axsegconlem9  28941  axpasch  28957  axeuclidlem  28978  axcontlem2  28981  axcontlem4  28983  axcontlem7  28986  axcontlem8  28987  finsumvtxdg2ssteplem4  29567  ipasslem2  30852  minvecolem2  30895  pjhthlem1  31411  wrdt2ind  32939  ccfldsrarelvec  33722  constrrtcclem  33776  circlemeth  34656  subfacval2  35193  subfaclim  35194  faclimlem1  35744  itgaddnc  37688  itgmulc2nc  37696  dvasin  37712  posbezout  42102  2np3bcnp1  42146  nnadddir  42310  nnmul1com  42311  nnmulcom  42312  sumcubes  42352  resubdi  42431  sn-negex12  42451  sn-mul01  42460  sn-mullid  42470  sn-0tie0  42474  sn-mul02  42475  renegmulnnass  42488  cnreeu  42505  fltmul  42650  cu3addd  42696  3cubeslem3l  42702  3cubeslem3r  42703  pellexlem6  42850  pell1234qrmulcl  42871  rmxyadd  42938  jm2.25  43016  relexpmulnn  43727  binomcxplemnotnn0  44380  sumnnodd  45650  dvnmul  45963  stoweidlem13  46033  wallispilem4  46088  wallispi2lem1  46091  wallispi2lem2  46092  stirlinglem1  46094  stirlinglem6  46099  stirlinglem7  46100  stirlinglem8  46101  stirlinglem10  46103  dirkerper  46116  dirkertrigeqlem1  46118  dirkertrigeqlem2  46119  dirkertrigeqlem3  46120  fourierdlem83  46209  hoidmvlelem2  46616  hspmbllem1  46646  smfmullem1  46811  deccarry  47328  fmtnorec4  47541  mod42tp1mod8  47594  lighneallem3  47599  opoeALTV  47675  opeoALTV  47676  2zlidl  48161  2zrngamgm  48166  altgsumbcALT  48274  itcovalpclem2  48597  ackval2  48608  affinecomb2  48629  itscnhlc0yqe  48685  itsclc0yqsollem1  48688  itsclc0yqsol  48690  itscnhlc0xyqsol  48691  itsclc0xyqsolr  48695  itscnhlinecirc02plem1  48708