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 7105 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1169 | 1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1284 ∈ wcel 1433 (class class class)co 5532 ℂcc 6979 + caddc 6984 · cmul 6986 |
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 7080 |
This theorem depends on definitions: df-bi 115 df-3an 921 |
This theorem is referenced by: subdi 7489 mulreim 7704 apadd1 7708 conjmulap 7817 cju 8038 flhalf 9304 modqcyc 9361 addmodlteq 9400 binom2 9585 binom3 9590 sqoddm1div8 9625 bcpasc 9693 remim 9747 mulreap 9751 readd 9756 remullem 9758 imadd 9764 cjadd 9771 bezoutlemnewy 10385 dvdsmulgcd 10414 lcmgcdlem 10459 |
Copyright terms: Public domain | W3C validator |