Theorem adddi 10891

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805   · cmul 10807

This theorem was proved from axioms:  ax-distr 10869

This theorem is referenced by:  adddir  10897  adddii  10918  adddid  10930  muladd11  11075  mul02lem1  11081  mul02  11083  muladd  11337  nnmulcl  11927  xadddilem  12957  expmul  13756  bernneq  13872  sqoddm1div8  13886  sqreulem  14999  isermulc2  15297  fsummulc2  15424  fsumcube  15698  efexp  15738  efi4p  15774  sinadd  15801  cosadd  15802  cos2tsin  15816  cos01bnd  15823  absefib  15835  efieq1re  15836  demoivreALT  15838  odd2np1  15978  opoe  16000  opeo  16002  gcdmultipleOLD  16188  pythagtriplem12  16455  cncrng  20531  cnlmod  24209  plydivlem4  25361  sinperlem  25542  cxpsqrt  25763  chtub  26265  bcp1ctr  26332  2lgslem3d1  26456  cncvcOLD  28846  hhph  29441  2zrngALT  45394