Theorem adddi 8013

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5923  ℂcc 7879   + caddc 7884   · cmul 7886

This theorem was proved from axioms:  ax-distr 7985

This theorem is referenced by:  adddir  8019  adddii  8038  adddid  8053  muladd11  8161  cnegex  8206  muladd  8412  nnmulcl  9013  expmul  10678  bernneq  10754  sqoddm1div8  10787  isermulc2  11507  efexp  11849  efi4p  11884  sinadd  11903  cosadd  11904  cos2tsin  11918  cos01bnd  11925  absefib  11938  efieq1re  11939  demoivreALT  11941  odd2np1  12040  opoe  12062  opeo  12064  gcdmultiple  12197  pythagtriplem12  12454  cncrng  14135  sinperlem  15054  2lgslem3d1  15351