Theorem adddi 8275

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146   · cmul 8148

This theorem was proved from axioms:  ax-distr 8247

This theorem is referenced by:  adddir  8281  adddii  8300  adddid  8314  muladd11  8423  cnegex  8468  muladd  8675  nnmulcl  9278  expmul  10973  bernneq  11050  sqoddm1div8  11083  isermulc2  12054  efexp  12397  efi4p  12432  sinadd  12451  cosadd  12452  cos2tsin  12466  cos01bnd  12473  absefib  12486  efieq1re  12487  demoivreALT  12489  odd2np1  12588  opoe  12610  opeo  12612  gcdmultiple  12745  pythagtriplem12  13002  cncrng  14847  sinperlem  15803  2lgslem3d1  16103