Theorem adddi 8305

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176   · cmul 8178

This theorem was proved from axioms:  ax-distr 8277

This theorem is referenced by:  adddir  8311  adddii  8330  adddid  8344  muladd11  8453  cnegex  8498  muladd  8705  nnmulcl  9308  expmul  11004  bernneq  11081  sqoddm1div8  11114  isermulc2  12089  efexp  12432  efi4p  12467  sinadd  12486  cosadd  12487  cos2tsin  12501  cos01bnd  12508  absefib  12521  efieq1re  12522  demoivreALT  12524  odd2np1  12623  opoe  12645  opeo  12647  gcdmultiple  12780  pythagtriplem12  13037  cncrng  14889  sinperlem  15892  2lgslem3d1  16202