Theorem adddi 8064

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930   + caddc 7935   · cmul 7937

This theorem was proved from axioms:  ax-distr 8036

This theorem is referenced by:  adddir  8070  adddii  8089  adddid  8104  muladd11  8212  cnegex  8257  muladd  8463  nnmulcl  9064  expmul  10736  bernneq  10812  sqoddm1div8  10845  isermulc2  11695  efexp  12037  efi4p  12072  sinadd  12091  cosadd  12092  cos2tsin  12106  cos01bnd  12113  absefib  12126  efieq1re  12127  demoivreALT  12129  odd2np1  12228  opoe  12250  opeo  12252  gcdmultiple  12385  pythagtriplem12  12642  cncrng  14375  sinperlem  15324  2lgslem3d1  15621