Theorem adddi 11118

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032   · cmul 11034

This theorem was proved from axioms:  ax-distr 11096

This theorem is referenced by:  adddir  11126  adddii  11148  adddid  11160  muladd11  11307  mul02lem1  11313  mul02  11315  muladd  11573  nnmulcl  12189  xadddilem  13237  expmul  14060  bernneq  14182  sqoddm1div8  14196  sqreulem  15313  isermulc2  15611  fsummulc2  15737  fsumcube  16016  efexp  16059  efi4p  16095  sinadd  16122  cosadd  16123  cos2tsin  16137  cos01bnd  16144  absefib  16156  efieq1re  16157  demoivreALT  16159  odd2np1  16301  opoe  16323  opeo  16325  pythagtriplem12  16788  cncrng  21378  cncrngOLD  21379  cnlmod  25117  plydivlem4  26273  sinperlem  26457  cxpsqrt  26680  chtub  27189  bcp1ctr  27256  2lgslem3d1  27380  cncvcOLD  30669  hhph  31264  2zrngALT  48742