Theorem adddi 10423

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  (class class class)co 6975  ℂcc 10332   + caddc 10337   · cmul 10339

This theorem was proved from axioms:  ax-distr 10401

This theorem is referenced by:  adddir  10429  adddii  10451  adddid  10463  muladd11  10609  mul02lem1  10615  mul02  10617  muladd  10872  nnmulcl  11463  xadddilem  12502  expmul  13288  bernneq  13404  sqoddm1div8  13418  sqreulem  14579  isermulc2  14874  fsummulc2  14998  fsumcube  15273  efexp  15313  efi4p  15349  sinadd  15376  cosadd  15377  cos2tsin  15391  cos01bnd  15398  absefib  15410  efieq1re  15411  demoivreALT  15413  odd2np1  15549  opoe  15571  opeo  15573  gcdmultiple  15755  pythagtriplem12  16018  cncrng  20284  cnlmod  23463  plydivlem4  24604  sinperlem  24785  cxpsqrt  25003  chtub  25506  bcp1ctr  25573  2lgslem3d1  25697  cncvcOLD  28153  hhph  28750  2zrngALT  43613