Theorem adddi 10628

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   + caddc 10542   · cmul 10544

This theorem was proved from axioms:  ax-distr 10606

This theorem is referenced by:  adddir  10634  adddii  10655  adddid  10667  muladd11  10812  mul02lem1  10818  mul02  10820  muladd  11074  nnmulcl  11664  xadddilem  12690  expmul  13477  bernneq  13593  sqoddm1div8  13607  sqreulem  14721  isermulc2  15016  fsummulc2  15141  fsumcube  15416  efexp  15456  efi4p  15492  sinadd  15519  cosadd  15520  cos2tsin  15534  cos01bnd  15541  absefib  15553  efieq1re  15554  demoivreALT  15556  odd2np1  15692  opoe  15714  opeo  15716  gcdmultipleOLD  15902  pythagtriplem12  16165  cncrng  20568  cnlmod  23746  plydivlem4  24887  sinperlem  25068  cxpsqrt  25288  chtub  25790  bcp1ctr  25857  2lgslem3d1  25981  cncvcOLD  28362  hhph  28957  2zrngALT  44226