Theorem adddi 8207

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078   · cmul 8080

This theorem was proved from axioms:  ax-distr 8179

This theorem is referenced by:  adddir  8213  adddii  8232  adddid  8247  muladd11  8355  cnegex  8400  muladd  8606  nnmulcl  9207  expmul  10890  bernneq  10966  sqoddm1div8  10999  isermulc2  11961  efexp  12304  efi4p  12339  sinadd  12358  cosadd  12359  cos2tsin  12373  cos01bnd  12380  absefib  12393  efieq1re  12394  demoivreALT  12396  odd2np1  12495  opoe  12517  opeo  12519  gcdmultiple  12652  pythagtriplem12  12909  cncrng  14645  sinperlem  15599  2lgslem3d1  15899