Theorem adddi 11199

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-distr 11177

This theorem is referenced by:  adddir  11205  adddii  11226  adddid  11238  muladd11  11384  mul02lem1  11390  mul02  11392  muladd  11646  nnmulcl  12236  xadddilem  13273  expmul  14073  bernneq  14192  sqoddm1div8  14206  sqreulem  15306  isermulc2  15604  fsummulc2  15730  fsumcube  16004  efexp  16044  efi4p  16080  sinadd  16107  cosadd  16108  cos2tsin  16122  cos01bnd  16129  absefib  16141  efieq1re  16142  demoivreALT  16144  odd2np1  16284  opoe  16306  opeo  16308  pythagtriplem12  16759  cncrng  20966  cnlmod  24656  plydivlem4  25809  sinperlem  25990  cxpsqrt  26211  chtub  26715  bcp1ctr  26782  2lgslem3d1  26906  cncvcOLD  29836  hhph  30431  2zrngALT  46846