Theorem adddid 8051

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 8011	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1249	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

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

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 7983

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

This theorem is referenced by:  subdi  8411  mulreim  8631  apadd1  8635  conjmulap  8756  cju  8988  flhalf  10392  modqcyc  10451  addmodlteq  10490  binom2  10743  binom3  10749  sqoddm1div8  10785  bcpasc  10858  remim  11025  mulreap  11029  readd  11034  remullem  11036  imadd  11042  cjadd  11049  bdtrilem  11404  fsummulc2  11613  binomlem  11648  tanval3ap  11879  sinadd  11901  tanaddap  11904  bezoutlemnewy  12163  dvdsmulgcd  12192  lcmgcdlem  12245  pythagtriplem1  12434  pcaddlem  12508  mul4sqlem  12562  tangtx  15074  rpmulcxp  15145  rpcxpmul2  15149  binom4  15215  lgseisenlem2  15312  2lgsoddprmlem2  15347  2sqlem4  15359  2sqlem8  15364