Theorem adddi 9904

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-distr 9882

This theorem is referenced by:  adddir  9910  adddii  9929  adddid  9943  muladd11  10085  mul02lem1  10091  mul02  10093  muladd  10341  nnmulcl  10920  xadddilem  11996  expmul  12767  bernneq  12852  sqoddm1div8  12890  sqreulem  13947  isermulc2  14236  fsummulc2  14358  fsumcube  14630  efexp  14670  efi4p  14706  sinadd  14733  cosadd  14734  cos2tsin  14748  cos01bnd  14755  absefib  14767  efieq1re  14768  demoivreALT  14770  odd2np1  14903  opoe  14925  opeo  14927  gcdmultiple  15107  pythagtriplem12  15369  cncrng  19586  cnlmod  22748  plydivlem4  23855  sinperlem  24036  cxpsqrt  24249  chtub  24737  bcp1ctr  24804  2lgslem3d1  24928  cncvcOLD  26822  hhph  27419  2zrngALT  41738