Theorem adddi 8164

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035   · cmul 8037

This theorem was proved from axioms:  ax-distr 8136

This theorem is referenced by:  adddir  8170  adddii  8189  adddid  8204  muladd11  8312  cnegex  8357  muladd  8563  nnmulcl  9164  expmul  10847  bernneq  10923  sqoddm1div8  10956  isermulc2  11902  efexp  12245  efi4p  12280  sinadd  12299  cosadd  12300  cos2tsin  12314  cos01bnd  12321  absefib  12334  efieq1re  12335  demoivreALT  12337  odd2np1  12436  opoe  12458  opeo  12460  gcdmultiple  12593  pythagtriplem12  12850  cncrng  14586  sinperlem  15535  2lgslem3d1  15832