Theorem adddi 8099

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 983   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970   · cmul 7972

This theorem was proved from axioms:  ax-distr 8071

This theorem is referenced by:  adddir  8105  adddii  8124  adddid  8139  muladd11  8247  cnegex  8292  muladd  8498  nnmulcl  9099  expmul  10773  bernneq  10849  sqoddm1div8  10882  isermulc2  11817  efexp  12159  efi4p  12194  sinadd  12213  cosadd  12214  cos2tsin  12228  cos01bnd  12235  absefib  12248  efieq1re  12249  demoivreALT  12251  odd2np1  12350  opoe  12372  opeo  12374  gcdmultiple  12507  pythagtriplem12  12764  cncrng  14498  sinperlem  15447  2lgslem3d1  15744