Theorem adddi 11292

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   + caddc 11206   · cmul 11208

This proof depends on axioms:  ax-distr 11270

This theorem is used by:  adddir  11300  adddii  11324  adddid  11336  muladd11  11483  mul02lem1  11489  mul02  11491  muladd  11751  nnmulcl  12362  xadddilem  13427  expmul  14253  bernneq  14376  sqoddm1div8  14390  sqreulem  15532  isermulc2  15830  fsummulc2  15955  fsumcube  16231  efexp  16274  efi4p  16310  sinadd  16337  cosadd  16338  cos2tsin  16352  cos01bnd  16359  absefib  16371  efieq1re  16372  demoivreALT  16374  odd2np1  16516  opoe  16538  opeo  16540  pythagtriplem12  17009  cncrng  21704  cnlmod  25466  plydivlem4  26622  sinperlem  26814  cxpsqrt  27036  chtub  27544  bcp1ctr  27611  2lgslem3d1  27735  cncvcOLD  31190  hhph  31785  2zrngALT  49444