Theorem adddi 11214

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  (class class class)co 7414  ℂcc 11123   + caddc 11128   · cmul 11130

This proof depends on axioms:  ax-distr 11192

This theorem is used by:  adddir  11222  adddii  11246  adddid  11258  muladd11  11405  mul02lem1  11411  mul02  11413  muladd  11671  nnmulcl  12282  xadddilem  13347  expmul  14172  bernneq  14294  sqoddm1div8  14308  sqreulem  15448  isermulc2  15746  fsummulc2  15871  fsumcube  16147  efexp  16190  efi4p  16226  sinadd  16253  cosadd  16254  cos2tsin  16268  cos01bnd  16275  absefib  16287  efieq1re  16288  demoivreALT  16290  odd2np1  16432  opoe  16454  opeo  16456  pythagtriplem12  16919  cncrng  21607  cnlmod  25369  plydivlem4  26527  sinperlem  26719  cxpsqrt  26941  chtub  27449  bcp1ctr  27516  2lgslem3d1  27640  cncvcOLD  31065  hhph  31660  2zrngALT  49170