Theorem adddi 8139

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010   · cmul 8012

This theorem was proved from axioms:  ax-distr 8111

This theorem is referenced by:  adddir  8145  adddii  8164  adddid  8179  muladd11  8287  cnegex  8332  muladd  8538  nnmulcl  9139  expmul  10814  bernneq  10890  sqoddm1div8  10923  isermulc2  11859  efexp  12201  efi4p  12236  sinadd  12255  cosadd  12256  cos2tsin  12270  cos01bnd  12277  absefib  12290  efieq1re  12291  demoivreALT  12293  odd2np1  12392  opoe  12414  opeo  12416  gcdmultiple  12549  pythagtriplem12  12806  cncrng  14541  sinperlem  15490  2lgslem3d1  15787