Theorem adddi 10615

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531

This theorem was proved from axioms:  ax-distr 10593

This theorem is referenced by:  adddir  10621  adddii  10642  adddid  10654  muladd11  10799  mul02lem1  10805  mul02  10807  muladd  11061  nnmulcl  11649  xadddilem  12675  expmul  13470  bernneq  13586  sqoddm1div8  13600  sqreulem  14711  isermulc2  15006  fsummulc2  15131  fsumcube  15406  efexp  15446  efi4p  15482  sinadd  15509  cosadd  15510  cos2tsin  15524  cos01bnd  15531  absefib  15543  efieq1re  15544  demoivreALT  15546  odd2np1  15682  opoe  15704  opeo  15706  gcdmultipleOLD  15890  pythagtriplem12  16153  cncrng  20112  cnlmod  23745  plydivlem4  24892  sinperlem  25073  cxpsqrt  25294  chtub  25796  bcp1ctr  25863  2lgslem3d1  25987  cncvcOLD  28366  hhph  28961  2zrngALT  44572