Theorem adddi 7893

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 973   = wceq 1348   ∈ wcel 2141  (class class class)co 5850  ℂcc 7759   + caddc 7764   · cmul 7766

This theorem was proved from axioms:  ax-distr 7865

This theorem is referenced by:  adddir  7898  adddii  7917  adddid  7931  muladd11  8039  cnegex  8084  muladd  8290  nnmulcl  8886  expmul  10508  bernneq  10583  sqoddm1div8  10616  isermulc2  11290  efexp  11632  efi4p  11667  sinadd  11686  cosadd  11687  cos2tsin  11701  cos01bnd  11708  absefib  11720  efieq1re  11721  demoivreALT  11723  odd2np1  11819  opoe  11841  opeo  11843  gcdmultiple  11962  pythagtriplem12  12216  sinperlem  13482