Theorem adddi 7938

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  (class class class)co 5870  ℂcc 7804   + caddc 7809   · cmul 7811

This theorem was proved from axioms:  ax-distr 7910

This theorem is referenced by:  adddir  7943  adddii  7962  adddid  7976  muladd11  8084  cnegex  8129  muladd  8335  nnmulcl  8934  expmul  10558  bernneq  10633  sqoddm1div8  10666  isermulc2  11339  efexp  11681  efi4p  11716  sinadd  11735  cosadd  11736  cos2tsin  11750  cos01bnd  11757  absefib  11769  efieq1re  11770  demoivreALT  11772  odd2np1  11868  opoe  11890  opeo  11892  gcdmultiple  12011  pythagtriplem12  12265  cncrng  13268  sinperlem  14011