Theorem adddi 11273

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   · cmul 11189

This theorem was proved from axioms:  ax-distr 11251

This theorem is referenced by:  adddir  11281  adddii  11302  adddid  11314  muladd11  11460  mul02lem1  11466  mul02  11468  muladd  11722  nnmulcl  12317  xadddilem  13356  expmul  14158  bernneq  14278  sqoddm1div8  14292  sqreulem  15408  isermulc2  15706  fsummulc2  15832  fsumcube  16108  efexp  16149  efi4p  16185  sinadd  16212  cosadd  16213  cos2tsin  16227  cos01bnd  16234  absefib  16246  efieq1re  16247  demoivreALT  16249  odd2np1  16389  opoe  16411  opeo  16413  pythagtriplem12  16873  cncrng  21424  cncrngOLD  21425  cnlmod  25192  plydivlem4  26356  sinperlem  26540  cxpsqrt  26763  chtub  27274  bcp1ctr  27341  2lgslem3d1  27465  cncvcOLD  30615  hhph  31210  2zrngALT  47977