Theorem adddi 11159

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   + caddc 11073   · cmul 11075

This theorem was proved from axioms:  ax-distr 11137

This theorem is referenced by:  adddir  11167  adddii  11191  adddid  11203  muladd11  11350  mul02lem1  11356  mul02  11358  muladd  11616  nnmulcl  12231  xadddilem  13294  expmul  14117  bernneq  14239  sqoddm1div8  14253  sqreulem  15370  isermulc2  15668  fsummulc2  15794  fsumcube  16073  efexp  16116  efi4p  16152  sinadd  16179  cosadd  16180  cos2tsin  16194  cos01bnd  16201  absefib  16213  efieq1re  16214  demoivreALT  16216  odd2np1  16358  opoe  16380  opeo  16382  pythagtriplem12  16845  cncrng  21425  cnlmod  25182  plydivlem4  26337  sinperlem  26522  cxpsqrt  26745  chtub  27253  bcp1ctr  27320  2lgslem3d1  27444  cncvcOLD  30732  hhph  31327  2zrngALT  48840