Theorem adddi 11217

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   + caddc 11131   · cmul 11133

This proof depends on axioms:  ax-distr 11195

This theorem is used by:  adddir  11225  adddii  11249  adddid  11261  muladd11  11408  mul02lem1  11414  mul02  11416  muladd  11674  nnmulcl  12285  xadddilem  13350  expmul  14175  bernneq  14297  sqoddm1div8  14311  sqreulem  15451  isermulc2  15749  fsummulc2  15874  fsumcube  16152  efexp  16195  efi4p  16231  sinadd  16258  cosadd  16259  cos2tsin  16273  cos01bnd  16280  absefib  16292  efieq1re  16293  demoivreALT  16295  odd2np1  16437  opoe  16459  opeo  16461  pythagtriplem12  16924  cncrng  21612  cnlmod  25374  plydivlem4  26533  sinperlem  26725  cxpsqrt  26948  chtub  27456  bcp1ctr  27523  2lgslem3d1  27647  cncvcOLD  31072  hhph  31667  2zrngALT  49177