Theorem adddi 11102

Description: Alias for ax-distr 11080, for naming consistency with adddii 11131. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
adddi	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddi

Step	Hyp	Ref	Expression
1		ax-distr 11080	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   + caddc 11016   · cmul 11018

This theorem was proved from axioms:  ax-distr 11080

This theorem is referenced by:  adddir  11110  adddii  11131  adddid  11143  muladd11  11290  mul02lem1  11296  mul02  11298  muladd  11556  nnmulcl  12156  xadddilem  13195  expmul  14016  bernneq  14138  sqoddm1div8  14152  sqreulem  15269  isermulc2  15567  fsummulc2  15693  fsumcube  15969  efexp  16012  efi4p  16048  sinadd  16075  cosadd  16076  cos2tsin  16090  cos01bnd  16097  absefib  16109  efieq1re  16110  demoivreALT  16112  odd2np1  16254  opoe  16276  opeo  16278  pythagtriplem12  16740  cncrng  21327  cncrngOLD  21328  cnlmod  25068  plydivlem4  26232  sinperlem  26417  cxpsqrt  26640  chtub  27151  bcp1ctr  27218  2lgslem3d1  27342  cncvcOLD  30565  hhph  31160  2zrngALT  48378