Theorem adddi 10960

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874   · cmul 10876

This theorem was proved from axioms:  ax-distr 10938

This theorem is referenced by:  adddir  10966  adddii  10987  adddid  10999  muladd11  11145  mul02lem1  11151  mul02  11153  muladd  11407  nnmulcl  11997  xadddilem  13028  expmul  13828  bernneq  13944  sqoddm1div8  13958  sqreulem  15071  isermulc2  15369  fsummulc2  15496  fsumcube  15770  efexp  15810  efi4p  15846  sinadd  15873  cosadd  15874  cos2tsin  15888  cos01bnd  15895  absefib  15907  efieq1re  15908  demoivreALT  15910  odd2np1  16050  opoe  16072  opeo  16074  gcdmultipleOLD  16260  pythagtriplem12  16527  cncrng  20619  cnlmod  24303  plydivlem4  25456  sinperlem  25637  cxpsqrt  25858  chtub  26360  bcp1ctr  26427  2lgslem3d1  26551  cncvcOLD  28945  hhph  29540  2zrngALT  45506