Theorem adddi 11244

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   + caddc 11158   · cmul 11160

This theorem was proved from axioms:  ax-distr 11222

This theorem is referenced by:  adddir  11252  adddii  11273  adddid  11285  muladd11  11431  mul02lem1  11437  mul02  11439  muladd  11695  nnmulcl  12290  xadddilem  13336  expmul  14148  bernneq  14268  sqoddm1div8  14282  sqreulem  15398  isermulc2  15694  fsummulc2  15820  fsumcube  16096  efexp  16137  efi4p  16173  sinadd  16200  cosadd  16201  cos2tsin  16215  cos01bnd  16222  absefib  16234  efieq1re  16235  demoivreALT  16237  odd2np1  16378  opoe  16400  opeo  16402  pythagtriplem12  16864  cncrng  21401  cncrngOLD  21402  cnlmod  25173  plydivlem4  26338  sinperlem  26522  cxpsqrt  26745  chtub  27256  bcp1ctr  27323  2lgslem3d1  27447  cncvcOLD  30602  hhph  31197  2zrngALT  48170