Theorem adddi 8030

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

Assertion

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

Proof of Theorem adddi

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

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

This theorem was proved from axioms:  ax-distr 8002

This theorem is referenced by:  adddir  8036  adddii  8055  adddid  8070  muladd11  8178  cnegex  8223  muladd  8429  nnmulcl  9030  expmul  10695  bernneq  10771  sqoddm1div8  10804  isermulc2  11524  efexp  11866  efi4p  11901  sinadd  11920  cosadd  11921  cos2tsin  11935  cos01bnd  11942  absefib  11955  efieq1re  11956  demoivreALT  11958  odd2np1  12057  opoe  12079  opeo  12081  gcdmultiple  12214  pythagtriplem12  12471  cncrng  14203  sinperlem  15152  2lgslem3d1  15449