Theorem adddi 8006

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877   · cmul 7879

This theorem was proved from axioms:  ax-distr 7978

This theorem is referenced by:  adddir  8012  adddii  8031  adddid  8046  muladd11  8154  cnegex  8199  muladd  8405  nnmulcl  9005  expmul  10658  bernneq  10734  sqoddm1div8  10767  isermulc2  11486  efexp  11828  efi4p  11863  sinadd  11882  cosadd  11883  cos2tsin  11897  cos01bnd  11904  absefib  11917  efieq1re  11918  demoivreALT  11920  odd2np1  12017  opoe  12039  opeo  12041  gcdmultiple  12160  pythagtriplem12  12416  cncrng  14068  sinperlem  14984  2lgslem3d1  15257