Theorem adddi 7745

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  (class class class)co 5767  ℂcc 7611   + caddc 7616   · cmul 7618

This theorem was proved from axioms:  ax-distr 7717

This theorem is referenced by:  adddir  7750  adddii  7769  adddid  7783  muladd11  7888  cnegex  7933  muladd  8139  nnmulcl  8734  expmul  10331  bernneq  10405  sqoddm1div8  10437  isermulc2  11102  efexp  11377  efi4p  11413  sinadd  11432  cosadd  11433  cos2tsin  11447  cos01bnd  11454  absefib  11466  efieq1re  11467  demoivreALT  11469  odd2np1  11559  opoe  11581  opeo  11583  gcdmultiple  11697  sinperlem  12878