Theorem adddi 8147

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018   · cmul 8020

This theorem was proved from axioms:  ax-distr 8119

This theorem is referenced by:  adddir  8153  adddii  8172  adddid  8187  muladd11  8295  cnegex  8340  muladd  8546  nnmulcl  9147  expmul  10823  bernneq  10899  sqoddm1div8  10932  isermulc2  11872  efexp  12214  efi4p  12249  sinadd  12268  cosadd  12269  cos2tsin  12283  cos01bnd  12290  absefib  12303  efieq1re  12304  demoivreALT  12306  odd2np1  12405  opoe  12427  opeo  12429  gcdmultiple  12562  pythagtriplem12  12819  cncrng  14554  sinperlem  15503  2lgslem3d1  15800