Theorem adddi 11105

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   + caddc 11019   · cmul 11021

This theorem was proved from axioms:  ax-distr 11083

This theorem is referenced by:  adddir  11113  adddii  11134  adddid  11146  muladd11  11293  mul02lem1  11299  mul02  11301  muladd  11559  nnmulcl  12159  xadddilem  13203  expmul  14024  bernneq  14146  sqoddm1div8  14160  sqreulem  15277  isermulc2  15575  fsummulc2  15701  fsumcube  15977  efexp  16020  efi4p  16056  sinadd  16083  cosadd  16084  cos2tsin  16098  cos01bnd  16105  absefib  16117  efieq1re  16118  demoivreALT  16120  odd2np1  16262  opoe  16284  opeo  16286  pythagtriplem12  16748  cncrng  21335  cncrngOLD  21336  cnlmod  25077  plydivlem4  26241  sinperlem  26426  cxpsqrt  26649  chtub  27160  bcp1ctr  27227  2lgslem3d1  27351  cncvcOLD  30574  hhph  31169  2zrngALT  48368