Theorem adddii 6835

Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ A ∈ ℂ
axi.2	⊢ B ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
adddii	⊢ (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))

Proof of Theorem adddii

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ A ∈ ℂ
2		axi.2	. 2 ⊢ B ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		adddi 6811	. 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))
5	1, 2, 3, 4	mp3an 1231	1 ⊢ (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))

Syntax hints:   = wceq 1242   ∈ wcel 1390  (class class class)co 5455  ℂcc 6709   + caddc 6714   · cmul 6716

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-distr 6787

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  3t3e9  7850  numltc  8163  numsucc  8169  numma  8174  4t3lem  8214  decbin2  8247  binom2i  9013