![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddid | GIF version |
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addassd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
adddid | ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addassd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | adddi 7464 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1174 | 1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1289 ∈ wcel 1438 (class class class)co 5644 ℂcc 7338 + caddc 7343 · cmul 7345 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-distr 7439 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: subdi 7853 mulreim 8071 apadd1 8075 conjmulap 8186 cju 8411 flhalf 9697 modqcyc 9754 addmodlteq 9793 binom2 10053 binom3 10059 sqoddm1div8 10094 bcpasc 10162 remim 10282 mulreap 10286 readd 10291 remullem 10293 imadd 10299 cjadd 10306 fsummulc2 10829 binomlem 10864 tanval3ap 10992 sinadd 11014 tanaddap 11017 bezoutlemnewy 11250 dvdsmulgcd 11279 lcmgcdlem 11324 |
Copyright terms: Public domain | W3C validator |