Theorem adddi 8157

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028   · cmul 8030

This theorem was proved from axioms:  ax-distr 8129

This theorem is referenced by:  adddir  8163  adddii  8182  adddid  8197  muladd11  8305  cnegex  8350  muladd  8556  nnmulcl  9157  expmul  10839  bernneq  10915  sqoddm1div8  10948  isermulc2  11894  efexp  12236  efi4p  12271  sinadd  12290  cosadd  12291  cos2tsin  12305  cos01bnd  12312  absefib  12325  efieq1re  12326  demoivreALT  12328  odd2np1  12427  opoe  12449  opeo  12451  gcdmultiple  12584  pythagtriplem12  12841  cncrng  14576  sinperlem  15525  2lgslem3d1  15822