Theorem adddi 11092

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   + caddc 11006   · cmul 11008

This theorem was proved from axioms:  ax-distr 11070

This theorem is referenced by:  adddir  11100  adddii  11121  adddid  11133  muladd11  11280  mul02lem1  11286  mul02  11288  muladd  11546  nnmulcl  12146  xadddilem  13190  expmul  14011  bernneq  14133  sqoddm1div8  14147  sqreulem  15264  isermulc2  15562  fsummulc2  15688  fsumcube  15964  efexp  16007  efi4p  16043  sinadd  16070  cosadd  16071  cos2tsin  16085  cos01bnd  16092  absefib  16104  efieq1re  16105  demoivreALT  16107  odd2np1  16249  opoe  16271  opeo  16273  pythagtriplem12  16735  cncrng  21323  cncrngOLD  21324  cnlmod  25065  plydivlem4  26229  sinperlem  26414  cxpsqrt  26637  chtub  27148  bcp1ctr  27215  2lgslem3d1  27339  cncvcOLD  30558  hhph  31153  2zrngALT  48284