Theorem adddi 8311

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182   · cmul 8184

This proof depends on axioms:  ax-distr 8283

This theorem is used by:  adddir  8317  adddii  8336  adddid  8350  muladd11  8459  cnegex  8504  muladd  8711  nnmulcl  9326  expmul  11023  bernneq  11100  sqoddm1div8  11133  isermulc2  12108  efexp  12451  efi4p  12486  sinadd  12505  cosadd  12506  cos2tsin  12520  cos01bnd  12527  absefib  12540  efieq1re  12541  demoivreALT  12543  odd2np1  12642  opoe  12664  opeo  12666  gcdmultiple  12799  pythagtriplem12  13056  cncrng  14908  sinperlem  15912  bcp1ctr  16126  2lgslem3d1  16231