Theorem adddi 7972

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2160  (class class class)co 5895  ℂcc 7838   + caddc 7843   · cmul 7845

This theorem was proved from axioms:  ax-distr 7944

This theorem is referenced by:  adddir  7977  adddii  7996  adddid  8011  muladd11  8119  cnegex  8164  muladd  8370  nnmulcl  8969  expmul  10595  bernneq  10671  sqoddm1div8  10704  isermulc2  11379  efexp  11721  efi4p  11756  sinadd  11775  cosadd  11776  cos2tsin  11790  cos01bnd  11797  absefib  11809  efieq1re  11810  demoivreALT  11812  odd2np1  11909  opoe  11931  opeo  11933  gcdmultiple  12052  pythagtriplem12  12306  cncrng  13869  sinperlem  14681