Theorem adddi 11177

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   + caddc 11091   · cmul 11093

This theorem was proved from axioms:  ax-distr 11155

This theorem is referenced by:  adddir  11185  adddii  11209  adddid  11221  muladd11  11368  mul02lem1  11374  mul02  11376  muladd  11634  nnmulcl  12248  xadddilem  13311  expmul  14134  bernneq  14256  sqoddm1div8  14270  sqreulem  15401  isermulc2  15699  fsummulc2  15825  fsumcube  16104  efexp  16147  efi4p  16183  sinadd  16210  cosadd  16211  cos2tsin  16225  cos01bnd  16232  absefib  16244  efieq1re  16245  demoivreALT  16247  odd2np1  16389  opoe  16411  opeo  16413  pythagtriplem12  16876  cncrng  21503  cnlmod  25260  plydivlem4  26418  sinperlem  26603  cxpsqrt  26826  chtub  27334  bcp1ctr  27401  2lgslem3d1  27525  cncvcOLD  30844  hhph  31439  2zrngALT  48874