Theorem adddi 8028

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   + caddc 7899   · cmul 7901

This theorem was proved from axioms:  ax-distr 8000

This theorem is referenced by:  adddir  8034  adddii  8053  adddid  8068  muladd11  8176  cnegex  8221  muladd  8427  nnmulcl  9028  expmul  10693  bernneq  10769  sqoddm1div8  10802  isermulc2  11522  efexp  11864  efi4p  11899  sinadd  11918  cosadd  11919  cos2tsin  11933  cos01bnd  11940  absefib  11953  efieq1re  11954  demoivreALT  11956  odd2np1  12055  opoe  12077  opeo  12079  gcdmultiple  12212  pythagtriplem12  12469  cncrng  14201  sinperlem  15128  2lgslem3d1  15425