Theorem adddi 11127

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-distr 11105

This theorem is referenced by:  adddir  11135  adddii  11156  adddid  11168  muladd11  11315  mul02lem1  11321  mul02  11323  muladd  11581  nnmulcl  12181  xadddilem  13221  expmul  14042  bernneq  14164  sqoddm1div8  14178  sqreulem  15295  isermulc2  15593  fsummulc2  15719  fsumcube  15995  efexp  16038  efi4p  16074  sinadd  16101  cosadd  16102  cos2tsin  16116  cos01bnd  16123  absefib  16135  efieq1re  16136  demoivreALT  16138  odd2np1  16280  opoe  16302  opeo  16304  pythagtriplem12  16766  cncrng  21355  cncrngOLD  21356  cnlmod  25108  plydivlem4  26272  sinperlem  26457  cxpsqrt  26680  chtub  27191  bcp1ctr  27258  2lgslem3d1  27382  cncvcOLD  30670  hhph  31265  2zrngALT  48608