Theorem adddi 11207

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

Assertion

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

Proof of Theorem adddi

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   + caddc 11121   · cmul 11123

This proof depends on axioms:  ax-distr 11185

This theorem is used by:  adddir  11215  adddii  11239  adddid  11251  muladd11  11398  mul02lem1  11404  mul02  11406  muladd  11664  nnmulcl  12275  xadddilem  13338  expmul  14163  bernneq  14285  sqoddm1div8  14299  sqreulem  15437  isermulc2  15735  fsummulc2  15861  fsumcube  16139  efexp  16182  efi4p  16218  sinadd  16245  cosadd  16246  cos2tsin  16260  cos01bnd  16267  absefib  16279  efieq1re  16280  demoivreALT  16282  odd2np1  16424  opoe  16446  opeo  16448  pythagtriplem12  16911  cncrng  21580  cnlmod  25336  plydivlem4  26494  sinperlem  26682  cxpsqrt  26905  chtub  27413  bcp1ctr  27480  2lgslem3d1  27604  cncvcOLD  30972  hhph  31567  2zrngALT  49060