Theorem adddid 10654

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  addid1  10809  cnegex  10810  addcom  10815  addcomd  10831  subdi  11062  conjmul  11346  cju  11621  flhalf  13195  modcyc  13269  addmodlteq  13309  binom3  13581  sqoddm1div8  13600  bcpasc  13677  hashf1lem2  13810  remim  14468  mulre  14472  readd  14477  remullem  14479  imadd  14485  cjadd  14492  sqreulem  14711  iseraltlem2  15031  o1fsum  15160  binomlem  15176  climcndslem2  15197  binomfallfaclem2  15386  bpoly4  15405  tanval3  15479  sinadd  15509  tanadd  15512  dvdsmulgcd  15895  lcmgcdlem  15940  pythagtriplem1  16143  pcaddlem  16214  prmreclem4  16245  prmreclem6  16247  mul4sqlem  16279  vdwlem3  16309  vdwlem6  16312  vdwlem9  16315  nn0srg  20161  rge0srg  20162  icopnfcnv  23547  pcoass  23629  cphipval2  23845  minveclem2  24030  pjthlem1  24041  ovolunlem1a  24100  ovolscalem1  24117  itgcnlem  24393  itgadd  24428  itgmulc2  24437  itgsplit  24439  aaliou3lem2  24939  abelthlem7  25033  tangtx  25098  efgh  25133  tanarg  25210  logcnlem4  25236  mulcxp  25276  cxpmul2  25280  heron  25424  quad2  25425  dcubic1lem  25429  dcubic2  25430  mcubic  25433  binom4  25436  quart1  25442  atanlogsublem  25501  2efiatan  25504  lgamgulmlem3  25616  basellem2  25667  basellem3  25668  basellem8  25673  chtub  25796  bposlem9  25876  lgseisenlem2  25960  2lgsoddprmlem2  25993  2sqlem4  26005  2sqlem8  26010  dchrisumlem1  26073  dchrvmasum2if  26081  dchrisum0re  26097  mulog2sumlem1  26118  selberglem1  26129  selberglem2  26130  selberg  26132  selberg2  26135  chpdifbndlem1  26137  selberg3lem1  26141  selberg4  26145  pntsval2  26160  pntibndlem2  26175  pntlemr  26186  pntlemf  26189  pntlemo  26191  ostth2lem2  26218  ostth2lem3  26219  brbtwn2  26699  axsegconlem9  26719  axpasch  26735  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  finsumvtxdg2ssteplem4  27338  ipasslem2  28615  minvecolem2  28658  pjhthlem1  29174  wrdt2ind  30653  ccfldsrarelvec  31144  circlemeth  32021  subfacval2  32547  subfaclim  32548  faclimlem1  33088  itgaddnc  35117  itgmulc2nc  35125  dvasin  35141  2np3bcnp1  39348  nnadddir  39471  nnmul1com  39472  nnmulcom  39473  resubdi  39534  sn-negex12  39553  sn-mul01  39562  sn-mulid2  39572  sn-0tie0  39576  sn-mul02  39577  cnreeu  39593  cu3addd  39621  3cubeslem3l  39627  3cubeslem3r  39628  pellexlem6  39775  pell1234qrmulcl  39796  rmxyadd  39862  jm2.25  39940  relexpmulnn  40410  binomcxplemnotnn0  41060  sumnnodd  42272  dvnmul  42585  stoweidlem13  42655  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem1  42716  stirlinglem6  42721  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  fourierdlem83  42831  hoidmvlelem2  43235  hspmbllem1  43265  smfmullem1  43423  deccarry  43868  fmtnorec4  44066  mod42tp1mod8  44120  lighneallem3  44125  opoeALTV  44201  opeoALTV  44202  2zlidl  44558  2zrngamgm  44563  altgsumbcALT  44755  itcovalpclem2  45085  ackval2  45096  affinecomb2  45117  itscnhlc0yqe  45173  itsclc0yqsollem1  45176  itsclc0yqsol  45178  itscnhlc0xyqsol  45179  itsclc0xyqsolr  45183  itscnhlinecirc02plem1  45196