Theorem adddi 11164

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

Assertion

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

Proof of Theorem adddi

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

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

This theorem was proved from axioms:  ax-distr 11142

This theorem is referenced by:  adddir  11172  adddii  11193  adddid  11205  muladd11  11351  mul02lem1  11357  mul02  11359  muladd  11617  nnmulcl  12217  xadddilem  13261  expmul  14079  bernneq  14201  sqoddm1div8  14215  sqreulem  15333  isermulc2  15631  fsummulc2  15757  fsumcube  16033  efexp  16076  efi4p  16112  sinadd  16139  cosadd  16140  cos2tsin  16154  cos01bnd  16161  absefib  16173  efieq1re  16174  demoivreALT  16176  odd2np1  16318  opoe  16340  opeo  16342  pythagtriplem12  16804  cncrng  21307  cncrngOLD  21308  cnlmod  25047  plydivlem4  26211  sinperlem  26396  cxpsqrt  26619  chtub  27130  bcp1ctr  27197  2lgslem3d1  27321  cncvcOLD  30519  hhph  31114  2zrngALT  48246