Theorem adddi 8258

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8124   + caddc 8129   · cmul 8131

This theorem was proved from axioms:  ax-distr 8230

This theorem is referenced by:  adddir  8264  adddii  8283  adddid  8297  muladd11  8405  cnegex  8450  muladd  8656  nnmulcl  9257  expmul  10945  bernneq  11021  sqoddm1div8  11054  isermulc2  12021  efexp  12364  efi4p  12399  sinadd  12418  cosadd  12419  cos2tsin  12433  cos01bnd  12440  absefib  12453  efieq1re  12454  demoivreALT  12456  odd2np1  12555  opoe  12577  opeo  12579  gcdmultiple  12712  pythagtriplem12  12969  cncrng  14709  sinperlem  15665  2lgslem3d1  15965