Theorem adddid 11336

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   + caddc 11206   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11493  cnegex  11494  addcom  11499  addcomd  11515  subdi  11752  conjmul  12037  cju  12319  nnadddir  12397  nnmul1com  12398  nnmulcom  12399  flhalf  13973  modcyc  14049  addmodlteq  14092  binom3  14371  sqoddm1div8  14390  bcpasc  14468  hashf1lem2  14604  remim  15289  mulre  15293  readd  15298  remullem  15300  imadd  15306  cjadd  15313  sqreulem  15532  iseraltlem2  15855  o1fsum  15985  binomlem  16003  climcndslem2  16024  binomfallfaclem2  16211  bpoly4  16230  tanval3  16307  sinadd  16337  tanadd  16340  dvdsmulgcd  16735  lcmgcdlem  16786  pythagtriplem1  16999  pcaddlem  17071  prmreclem4  17102  prmreclem6  17104  mul4sqlem  17136  vdwlem3  17166  vdwlem6  17169  vdwlem9  17172  nn0srg  21748  rge0srg  21749  mhppwdeg  22476  icopnfcnv  25268  pcoass  25350  cphipval2  25567  minveclem2  25752  pjthlem1  25763  ovolunlem1a  25822  ovolscalem1  25839  itgcnlem  26115  itgadd  26150  itgmulc2  26159  itgsplit  26161  aaliou3lem2  26675  abelthlem7  26770  tangtx  26839  efgh  26874  tanarg  26952  logcnlem4  26978  mulcxp  27018  cxpmul2  27022  heron  27171  quad2  27172  dcubic1lem  27176  dcubic2  27177  mcubic  27180  binom4  27183  quart1  27189  atanlogsublem  27248  2efiatan  27251  lgamgulmlem3  27363  basellem2  27414  basellem3  27415  basellem8  27420  chtub  27544  bposlem9  27624  lgseisenlem2  27708  2lgsoddprmlem2  27741  2sqlem4  27753  2sqlem8  27758  dchrisumlem1  27821  dchrvmasum2if  27829  dchrisum0re  27845  mulog2sumlem1  27866  selberglem1  27877  selberglem2  27878  selberg  27880  selberg2  27883  chpdifbndlem1  27885  selberg3lem1  27889  selberg4  27893  pntsval2  27908  pntibndlem2  27923  pntlemr  27934  pntlemf  27937  pntlemo  27939  ostth2lem2  27966  ostth2lem3  27967  brbtwn2  29488  axsegconlem9  29508  axpasch  29524  axeuclidlem  29545  axcontlem2  29548  axcontlem4  29550  axcontlem7  29553  axcontlem8  29554  finsumvtxdg2ssteplem4  30134  ipasslem2  31439  minvecolem2  31482  pjhthlem1  31998  wrdt2ind  33562  ccfldsrarelvec  34349  constrrtcclem  34412  constrremulcl  34445  constrrecl  34447  circlemeth  35315  subfacval2  36038  subfaclim  36039  faclimlem1  36600  itgaddnc  38691  itgmulc2nc  38699  dvasin  38715  posbezout  43243  2np3bcnp1  43287  quadfac  43348  sumcubes  43463  resubdi  43540  sn-negex12  43561  sn-mul01  43570  sn-mullid  43580  redivdird  43606  sn-0tie0  43608  sn-mul02  43609  renegmulnnass  43622  cnreeu  43647  fltmul  43764  cu3addd  43784  3cubeslem3l  43789  3cubeslem3r  43790  pellexlem6  43934  pell1234qrmulcl  43955  rmxyadd  44021  jm2.25  44099  relexpmulnn  44802  binomcxplemnotnn0  45433  sumnnodd  46735  dvnmul  47046  stoweidlem13  47116  wallispilem4  47171  wallispi2lem1  47174  wallispi2lem2  47175  stirlinglem1  47177  stirlinglem6  47182  stirlinglem7  47183  stirlinglem8  47184  stirlinglem10  47186  dirkerper  47199  dirkertrigeqlem1  47201  dirkertrigeqlem2  47202  dirkertrigeqlem3  47203  fourierdlem83  47292  hoidmvlelem2  47699  hspmbllem1  47729  smfmullem1  47894  sin5tlem4  48015  deccarry  48474  fmtnorec4  48727  mod42tp1mod8  48780  lighneallem3  48785  opoeALTV  48874  opeoALTV  48875  2zlidl  49430  2zrngamgm  49435  altgsumbcALT  49558  itcovalpclem2  49876  ackval2  49887  affinecomb2  49908  itscnhlc0yqe  49964  itsclc0yqsollem1  49967  itsclc0yqsol  49969  itscnhlc0xyqsol  49970  itsclc0xyqsolr  49974  itscnhlinecirc02plem1  49987