Theorem adddi 11198

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107   + caddc 11112   · cmul 11114

This theorem was proved from axioms:  ax-distr 11176

This theorem is referenced by:  adddir  11204  adddii  11225  adddid  11237  muladd11  11383  mul02lem1  11389  mul02  11391  muladd  11645  nnmulcl  12235  xadddilem  13272  expmul  14072  bernneq  14191  sqoddm1div8  14205  sqreulem  15305  isermulc2  15603  fsummulc2  15729  fsumcube  16003  efexp  16043  efi4p  16079  sinadd  16106  cosadd  16107  cos2tsin  16121  cos01bnd  16128  absefib  16140  efieq1re  16141  demoivreALT  16143  odd2np1  16283  opoe  16305  opeo  16307  pythagtriplem12  16758  cncrng  20965  cnlmod  24655  plydivlem4  25808  sinperlem  25989  cxpsqrt  26210  chtub  26712  bcp1ctr  26779  2lgslem3d1  26903  cncvcOLD  29831  hhph  30426  2zrngALT  46836