Theorem adddi 8318

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

Assertion

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

Proof of Theorem adddi

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

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

This proof depends on axioms:  ax-distr 8290

This theorem is used by:  adddir  8324  adddii  8343  adddid  8357  muladd11  8467  cnegex  8512  muladd  8719  nnmulcl  9335  expmul  11042  bernneq  11119  sqoddm1div8  11152  isermulc2  12131  efexp  12474  efi4p  12509  sinadd  12528  cosadd  12529  cos2tsin  12543  cos01bnd  12550  absefib  12563  efieq1re  12564  demoivreALT  12566  odd2np1  12665  opoe  12687  opeo  12689  gcdmultiple  12822  pythagtriplem12  13083  cncrng  15015  sinperlem  16068  chtqub  16329  bcp1ctr  16339  2lgslem3d1  16457