Theorem adddi 7910

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 974   = wceq 1349   ∈ wcel 2142  (class class class)co 5857  ℂcc 7776   + caddc 7781   · cmul 7783

This theorem was proved from axioms:  ax-distr 7882

This theorem is referenced by:  adddir  7915  adddii  7934  adddid  7948  muladd11  8056  cnegex  8101  muladd  8307  nnmulcl  8903  expmul  10525  bernneq  10600  sqoddm1div8  10633  isermulc2  11307  efexp  11649  efi4p  11684  sinadd  11703  cosadd  11704  cos2tsin  11718  cos01bnd  11725  absefib  11737  efieq1re  11738  demoivreALT  11740  odd2np1  11836  opoe  11858  opeo  11860  gcdmultiple  11979  pythagtriplem12  12233  sinperlem  13608