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  11043  bernneq  11120  sqoddm1div8  11153  isermulc2  12132  efexp  12475  efi4p  12510  sinadd  12529  cosadd  12530  cos2tsin  12544  cos01bnd  12551  absefib  12564  efieq1re  12565  demoivreALT  12567  odd2np1  12666  opoe  12688  opeo  12690  gcdmultiple  12823  pythagtriplem12  13084  cncrng  15016  sinperlem  16047  chtqub  16308  bcp1ctr  16318  2lgslem3d1  16436