Theorem adddi 8312

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   + caddc 8183   · cmul 8185

This proof depends on axioms:  ax-distr 8284

This theorem is used by:  adddir  8318  adddii  8337  adddid  8351  muladd11  8461  cnegex  8506  muladd  8713  nnmulcl  9328  expmul  11035  bernneq  11112  sqoddm1div8  11145  isermulc2  12124  efexp  12467  efi4p  12502  sinadd  12521  cosadd  12522  cos2tsin  12536  cos01bnd  12543  absefib  12556  efieq1re  12557  demoivreALT  12559  odd2np1  12658  opoe  12680  opeo  12682  gcdmultiple  12815  pythagtriplem12  13076  cncrng  14957  sinperlem  15962  chtqub  16218  bcp1ctr  16228  2lgslem3d1  16341