Theorem adddi 11190

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   + caddc 11104   · cmul 11106

This theorem was proved from axioms:  ax-distr 11168

This theorem is referenced by:  adddir  11198  adddii  11222  adddid  11234  muladd11  11381  mul02lem1  11387  mul02  11389  muladd  11647  nnmulcl  12258  xadddilem  13321  expmul  14145  bernneq  14267  sqoddm1div8  14281  sqreulem  15413  isermulc2  15711  fsummulc2  15837  fsumcube  16115  efexp  16158  efi4p  16194  sinadd  16221  cosadd  16222  cos2tsin  16236  cos01bnd  16243  absefib  16255  efieq1re  16256  demoivreALT  16258  odd2np1  16400  opoe  16422  opeo  16424  pythagtriplem12  16887  cncrng  21524  cnlmod  25280  plydivlem4  26438  sinperlem  26626  cxpsqrt  26849  chtub  27357  bcp1ctr  27424  2lgslem3d1  27548  cncvcOLD  30916  hhph  31511  2zrngALT  49002