Theorem adddi 7537

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 925   = wceq 1290   ∈ wcel 1439  (class class class)co 5668  ℂcc 7411   + caddc 7416   · cmul 7418

This theorem was proved from axioms:  ax-distr 7512

This theorem is referenced by:  adddir  7542  adddii  7561  adddid  7575  muladd11  7678  cnegex  7723  muladd  7925  nnmulcl  8506  expmul  10063  bernneq  10137  sqoddm1div8  10169  iisermulc2  10791  efexp  11035  efi4p  11071  sinadd  11090  cosadd  11091  cos2tsin  11105  cos01bnd  11112  absefib  11123  efieq1re  11124  demoivreALT  11126  odd2np1  11214  opoe  11236  opeo  11238  gcdmultiple  11350