Theorem adddi 11319

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  (class class class)co 7446  ℂcc 11228   + caddc 11233   · cmul 11235

This proof depends on axioms:  ax-distr 11297

This theorem is used by:  adddir  11327  adddii  11351  adddid  11363  muladd11  11510  mul02lem1  11516  mul02  11518  muladd  11778  nnmulcl  12389  xadddilem  13454  expmul  14280  bernneq  14403  sqoddm1div8  14417  sqreulem  15559  isermulc2  15857  fsummulc2  15982  fsumcube  16258  efexp  16301  efi4p  16337  sinadd  16364  cosadd  16365  cos2tsin  16379  cos01bnd  16386  absefib  16398  efieq1re  16399  demoivreALT  16401  odd2np1  16543  opoe  16565  opeo  16567  pythagtriplem12  17036  cncrng  21732  cnlmod  25494  plydivlem4  26650  sinperlem  26842  cxpsqrt  27064  chtub  27572  bcp1ctr  27639  2lgslem3d1  27763  cncvcOLD  31218  hhph  31813  2zrngALT  49566  sinhadd  51138  coshadd  51139