Theorem adddi 11127

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-distr 11105

This theorem is referenced by:  adddir  11135  adddii  11157  adddid  11169  muladd11  11316  mul02lem1  11322  mul02  11324  muladd  11582  nnmulcl  12198  xadddilem  13246  expmul  14069  bernneq  14191  sqoddm1div8  14205  sqreulem  15322  isermulc2  15620  fsummulc2  15746  fsumcube  16025  efexp  16068  efi4p  16104  sinadd  16131  cosadd  16132  cos2tsin  16146  cos01bnd  16153  absefib  16165  efieq1re  16166  demoivreALT  16168  odd2np1  16310  opoe  16332  opeo  16334  pythagtriplem12  16797  cncrng  21373  cnlmod  25107  plydivlem4  26262  sinperlem  26444  cxpsqrt  26667  chtub  27175  bcp1ctr  27242  2lgslem3d1  27366  cncvcOLD  30654  hhph  31249  2zrngALT  48730