Theorem adddid 11205

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078   · cmul 11080

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

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

This theorem is referenced by:  addrid  11361  cnegex  11362  addcom  11367  addcomd  11383  subdi  11618  conjmul  11906  cju  12189  flhalf  13799  modcyc  13875  addmodlteq  13918  binom3  14196  sqoddm1div8  14215  bcpasc  14293  hashf1lem2  14428  remim  15090  mulre  15094  readd  15099  remullem  15101  imadd  15107  cjadd  15114  sqreulem  15333  iseraltlem2  15656  o1fsum  15786  binomlem  15802  climcndslem2  15823  binomfallfaclem2  16013  bpoly4  16032  tanval3  16109  sinadd  16139  tanadd  16142  dvdsmulgcd  16533  lcmgcdlem  16583  pythagtriplem1  16794  pcaddlem  16866  prmreclem4  16897  prmreclem6  16899  mul4sqlem  16931  vdwlem3  16961  vdwlem6  16964  vdwlem9  16967  nn0srg  21361  rge0srg  21362  mhppwdeg  22044  icopnfcnv  24847  pcoass  24931  cphipval2  25148  minveclem2  25333  pjthlem1  25344  ovolunlem1a  25404  ovolscalem1  25421  itgcnlem  25698  itgadd  25733  itgmulc2  25742  itgsplit  25744  aaliou3lem2  26258  abelthlem7  26355  tangtx  26421  efgh  26457  tanarg  26535  logcnlem4  26561  mulcxp  26601  cxpmul2  26605  heron  26755  quad2  26756  dcubic1lem  26760  dcubic2  26761  mcubic  26764  binom4  26767  quart1  26773  atanlogsublem  26832  2efiatan  26835  lgamgulmlem3  26948  basellem2  26999  basellem3  27000  basellem8  27005  chtub  27130  bposlem9  27210  lgseisenlem2  27294  2lgsoddprmlem2  27327  2sqlem4  27339  2sqlem8  27344  dchrisumlem1  27407  dchrvmasum2if  27415  dchrisum0re  27431  mulog2sumlem1  27452  selberglem1  27463  selberglem2  27464  selberg  27466  selberg2  27469  chpdifbndlem1  27471  selberg3lem1  27475  selberg4  27479  pntsval2  27494  pntibndlem2  27509  pntlemr  27520  pntlemf  27523  pntlemo  27525  ostth2lem2  27552  ostth2lem3  27553  brbtwn2  28839  axsegconlem9  28859  axpasch  28875  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  finsumvtxdg2ssteplem4  29483  ipasslem2  30768  minvecolem2  30811  pjhthlem1  31327  wrdt2ind  32882  ccfldsrarelvec  33673  constrrtcclem  33731  constrremulcl  33764  constrrecl  33766  circlemeth  34638  subfacval2  35181  subfaclim  35182  faclimlem1  35737  itgaddnc  37681  itgmulc2nc  37689  dvasin  37705  posbezout  42095  2np3bcnp1  42139  nnadddir  42265  nnmul1com  42266  nnmulcom  42267  sumcubes  42308  resubdi  42391  sn-negex12  42412  sn-mul01  42421  sn-mullid  42431  sn-0tie0  42446  sn-mul02  42447  renegmulnnass  42460  cnreeu  42485  fltmul  42630  cu3addd  42676  3cubeslem3l  42681  3cubeslem3r  42682  pellexlem6  42829  pell1234qrmulcl  42850  rmxyadd  42917  jm2.25  42995  relexpmulnn  43705  binomcxplemnotnn0  44352  sumnnodd  45635  dvnmul  45948  stoweidlem13  46018  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem1  46079  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  fourierdlem83  46194  hoidmvlelem2  46601  hspmbllem1  46631  smfmullem1  46796  deccarry  47316  fmtnorec4  47554  mod42tp1mod8  47607  lighneallem3  47612  opoeALTV  47688  opeoALTV  47689  2zlidl  48232  2zrngamgm  48237  altgsumbcALT  48345  itcovalpclem2  48664  ackval2  48675  affinecomb2  48696  itscnhlc0yqe  48752  itsclc0yqsollem1  48755  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itsclc0xyqsolr  48762  itscnhlinecirc02plem1  48775