Theorem adddid 11251

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121   · cmul 11123

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

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

This theorem is used by:  addrid  11408  cnegex  11409  addcom  11414  addcomd  11430  subdi  11665  conjmul  11950  cju  12232  nnadddir  12310  nnmul1com  12311  nnmulcom  12312  flhalf  13883  modcyc  13959  addmodlteq  14002  binom3  14280  sqoddm1div8  14299  bcpasc  14377  hashf1lem2  14513  remim  15194  mulre  15198  readd  15203  remullem  15205  imadd  15211  cjadd  15218  sqreulem  15437  iseraltlem2  15760  o1fsum  15891  binomlem  15909  climcndslem2  15930  binomfallfaclem2  16119  bpoly4  16138  tanval3  16215  sinadd  16245  tanadd  16248  dvdsmulgcd  16639  lcmgcdlem  16689  pythagtriplem1  16901  pcaddlem  16973  prmreclem4  17004  prmreclem6  17006  mul4sqlem  17038  vdwlem3  17068  vdwlem6  17071  vdwlem9  17074  nn0srg  21624  rge0srg  21625  mhppwdeg  22350  icopnfcnv  25138  pcoass  25220  cphipval2  25437  minveclem2  25622  pjthlem1  25633  ovolunlem1a  25692  ovolscalem1  25709  itgcnlem  25986  itgadd  26021  itgmulc2  26030  itgsplit  26032  aaliou3lem2  26543  abelthlem7  26638  tangtx  26707  efgh  26743  tanarg  26821  logcnlem4  26847  mulcxp  26887  cxpmul2  26891  heron  27040  quad2  27041  dcubic1lem  27045  dcubic2  27046  mcubic  27049  binom4  27052  quart1  27058  atanlogsublem  27117  2efiatan  27120  lgamgulmlem3  27232  basellem2  27283  basellem3  27284  basellem8  27289  chtub  27413  bposlem9  27493  lgseisenlem2  27577  2lgsoddprmlem2  27610  2sqlem4  27622  2sqlem8  27627  dchrisumlem1  27690  dchrvmasum2if  27698  dchrisum0re  27714  mulog2sumlem1  27735  selberglem1  27746  selberglem2  27747  selberg  27749  selberg2  27752  chpdifbndlem1  27754  selberg3lem1  27758  selberg4  27762  pntsval2  27777  pntibndlem2  27792  pntlemr  27803  pntlemf  27806  pntlemo  27808  ostth2lem2  27835  ostth2lem3  27836  brbtwn2  29292  axsegconlem9  29312  axpasch  29328  axeuclidlem  29349  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem8  29358  finsumvtxdg2ssteplem4  29935  ipasslem2  31221  minvecolem2  31264  pjhthlem1  31780  wrdt2ind  33306  ccfldsrarelvec  34092  constrrtcclem  34155  constrremulcl  34188  constrrecl  34190  circlemeth  35059  subfacval2  35700  subfaclim  35701  faclimlem1  36256  itgaddnc  38372  itgmulc2nc  38380  dvasin  38396  posbezout  42908  2np3bcnp1  42952  quadfac  43013  sumcubes  43115  resubdi  43198  sn-negex12  43219  sn-mul01  43228  sn-mullid  43238  redivdird  43264  sn-0tie0  43266  sn-mul02  43267  renegmulnnass  43280  cnreeu  43305  fltmul  43408  cu3addd  43453  3cubeslem3l  43458  3cubeslem3r  43459  pellexlem6  43602  pell1234qrmulcl  43623  rmxyadd  43689  jm2.25  43767  relexpmulnn  44476  binomcxplemnotnn0  45107  sumnnodd  46387  dvnmul  46698  stoweidlem13  46768  wallispilem4  46823  wallispi2lem1  46826  wallispi2lem2  46827  stirlinglem1  46829  stirlinglem6  46834  stirlinglem7  46835  stirlinglem8  46836  stirlinglem10  46838  dirkerper  46851  dirkertrigeqlem1  46853  dirkertrigeqlem2  46854  dirkertrigeqlem3  46855  fourierdlem83  46944  hoidmvlelem2  47351  hspmbllem1  47381  smfmullem1  47546  sin5tlem4  47654  deccarry  48089  fmtnorec4  48342  mod42tp1mod8  48395  lighneallem3  48400  opoeALTV  48489  opeoALTV  48490  2zlidl  49046  2zrngamgm  49051  altgsumbcALT  49174  itcovalpclem2  49492  ackval2  49503  affinecomb2  49524  itscnhlc0yqe  49580  itsclc0yqsollem1  49583  itsclc0yqsol  49585  itscnhlc0xyqsol  49586  itsclc0xyqsolr  49590  itscnhlinecirc02plem1  49603