Theorem adddi 11218

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   + caddc 11132   · cmul 11134

This theorem was proved from axioms:  ax-distr 11196

This theorem is referenced by:  adddir  11226  adddii  11247  adddid  11259  muladd11  11405  mul02lem1  11411  mul02  11413  muladd  11669  nnmulcl  12264  xadddilem  13310  expmul  14125  bernneq  14247  sqoddm1div8  14261  sqreulem  15378  isermulc2  15674  fsummulc2  15800  fsumcube  16076  efexp  16119  efi4p  16155  sinadd  16182  cosadd  16183  cos2tsin  16197  cos01bnd  16204  absefib  16216  efieq1re  16217  demoivreALT  16219  odd2np1  16360  opoe  16382  opeo  16384  pythagtriplem12  16846  cncrng  21351  cncrngOLD  21352  cnlmod  25091  plydivlem4  26256  sinperlem  26441  cxpsqrt  26664  chtub  27175  bcp1ctr  27242  2lgslem3d1  27366  cncvcOLD  30564  hhph  31159  2zrngALT  48229