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 7865 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1220 | 1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1335 ∈ wcel 2128 (class class class)co 5825 ℂcc 7731 + caddc 7736 · cmul 7738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-distr 7837 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: subdi 8261 mulreim 8480 apadd1 8484 conjmulap 8603 cju 8833 flhalf 10205 modqcyc 10262 addmodlteq 10301 binom2 10533 binom3 10539 sqoddm1div8 10575 bcpasc 10644 remim 10764 mulreap 10768 readd 10773 remullem 10775 imadd 10781 cjadd 10788 bdtrilem 11142 fsummulc2 11349 binomlem 11384 tanval3ap 11615 sinadd 11637 tanaddap 11640 bezoutlemnewy 11884 dvdsmulgcd 11913 lcmgcdlem 11958 pythagtriplem1 12144 tangtx 13201 rpmulcxp 13272 binom4 13338 |
Copyright terms: Public domain | W3C validator |