Theorem adddi 8011

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

Assertion

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

Proof of Theorem adddi

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   + caddc 7882   · cmul 7884

This theorem was proved from axioms:  ax-distr 7983

This theorem is referenced by:  adddir  8017  adddii  8036  adddid  8051  muladd11  8159  cnegex  8204  muladd  8410  nnmulcl  9011  expmul  10676  bernneq  10752  sqoddm1div8  10785  isermulc2  11505  efexp  11847  efi4p  11882  sinadd  11901  cosadd  11902  cos2tsin  11916  cos01bnd  11923  absefib  11936  efieq1re  11937  demoivreALT  11939  odd2np1  12038  opoe  12060  opeo  12062  gcdmultiple  12187  pythagtriplem12  12444  cncrng  14125  sinperlem  15044  2lgslem3d1  15341