Theorem adddi 11125

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   + caddc 11039   · cmul 11041

This theorem was proved from axioms:  ax-distr 11103

This theorem is referenced by:  adddir  11133  adddii  11155  adddid  11167  muladd11  11314  mul02lem1  11320  mul02  11322  muladd  11580  nnmulcl  12196  xadddilem  13244  expmul  14067  bernneq  14189  sqoddm1div8  14203  sqreulem  15320  isermulc2  15618  fsummulc2  15744  fsumcube  16023  efexp  16066  efi4p  16102  sinadd  16129  cosadd  16130  cos2tsin  16144  cos01bnd  16151  absefib  16163  efieq1re  16164  demoivreALT  16166  odd2np1  16308  opoe  16330  opeo  16332  pythagtriplem12  16795  cncrng  21375  cnlmod  25132  plydivlem4  26287  sinperlem  26469  cxpsqrt  26692  chtub  27200  bcp1ctr  27267  2lgslem3d1  27391  cncvcOLD  30679  hhph  31274  2zrngALT  48752