Theorem adddid 8247

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddid	⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddi 8207	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1274	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078   · cmul 8080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8179

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  subdi  8607  mulreim  8827  apadd1  8831  conjmulap  8952  cju  9184  flhalf  10606  modqcyc  10665  addmodlteq  10704  binom2  10957  binom3  10963  sqoddm1div8  10999  bcpasc  11072  remim  11481  mulreap  11485  readd  11490  remullem  11492  imadd  11498  cjadd  11505  bdtrilem  11860  fsummulc2  12070  binomlem  12105  tanval3ap  12336  sinadd  12358  tanaddap  12361  bezoutlemnewy  12628  dvdsmulgcd  12657  lcmgcdlem  12710  pythagtriplem1  12899  pcaddlem  12973  mul4sqlem  13027  tangtx  15629  rpmulcxp  15700  rpcxpmul2  15704  binom4  15770  lgseisenlem2  15870  2lgsoddprmlem2  15905  2sqlem4  15917  2sqlem8  15922