Theorem adddi 11270

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   + caddc 11184   · cmul 11186

This proof depends on axioms:  ax-distr 11248

This theorem is used by:  adddir  11278  adddii  11302  adddid  11314  muladd11  11461  mul02lem1  11467  mul02  11469  muladd  11729  nnmulcl  12340  xadddilem  13405  expmul  14230  bernneq  14353  sqoddm1div8  14367  sqreulem  15507  isermulc2  15805  fsummulc2  15930  fsumcube  16206  efexp  16249  efi4p  16285  sinadd  16312  cosadd  16313  cos2tsin  16327  cos01bnd  16334  absefib  16346  efieq1re  16347  demoivreALT  16349  odd2np1  16491  opoe  16513  opeo  16515  pythagtriplem12  16984  cncrng  21679  cnlmod  25441  plydivlem4  26599  sinperlem  26791  cxpsqrt  27013  chtub  27521  bcp1ctr  27588  2lgslem3d1  27712  cncvcOLD  31167  hhph  31762  2zrngALT  49295