Theorem adddi 11115

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031

This theorem was proved from axioms:  ax-distr 11093

This theorem is referenced by:  adddir  11123  adddii  11144  adddid  11156  muladd11  11303  mul02lem1  11309  mul02  11311  muladd  11569  nnmulcl  12169  xadddilem  13209  expmul  14030  bernneq  14152  sqoddm1div8  14166  sqreulem  15283  isermulc2  15581  fsummulc2  15707  fsumcube  15983  efexp  16026  efi4p  16062  sinadd  16089  cosadd  16090  cos2tsin  16104  cos01bnd  16111  absefib  16123  efieq1re  16124  demoivreALT  16126  odd2np1  16268  opoe  16290  opeo  16292  pythagtriplem12  16754  cncrng  21343  cncrngOLD  21344  cnlmod  25096  plydivlem4  26260  sinperlem  26445  cxpsqrt  26668  chtub  27179  bcp1ctr  27246  2lgslem3d1  27370  cncvcOLD  30658  hhph  31253  2zrngALT  48496