Theorem adddi 11117

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031   · cmul 11033

This theorem was proved from axioms:  ax-distr 11095

This theorem is referenced by:  adddir  11125  adddii  11146  adddid  11158  muladd11  11304  mul02lem1  11310  mul02  11312  muladd  11570  nnmulcl  12170  xadddilem  13214  expmul  14032  bernneq  14154  sqoddm1div8  14168  sqreulem  15285  isermulc2  15583  fsummulc2  15709  fsumcube  15985  efexp  16028  efi4p  16064  sinadd  16091  cosadd  16092  cos2tsin  16106  cos01bnd  16113  absefib  16125  efieq1re  16126  demoivreALT  16128  odd2np1  16270  opoe  16292  opeo  16294  pythagtriplem12  16756  cncrng  21313  cncrngOLD  21314  cnlmod  25056  plydivlem4  26220  sinperlem  26405  cxpsqrt  26628  chtub  27139  bcp1ctr  27206  2lgslem3d1  27330  cncvcOLD  30545  hhph  31140  2zrngALT  48239