![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adddii | Structured version Visualization version GIF version |
Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
axi.3 | ⊢ 𝐶 ∈ ℂ |
Ref | Expression |
---|---|
adddii | ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | axi.3 | . 2 ⊢ 𝐶 ∈ ℂ | |
4 | adddi 10361 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1534 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∈ wcel 2106 (class class class)co 6922 ℂcc 10270 + caddc 10275 · cmul 10277 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 10339 |
This theorem depends on definitions: df-bi 199 df-an 387 df-3an 1073 |
This theorem is referenced by: addid1 10556 3t3e9 11549 numltc 11872 numsucc 11886 numma 11890 decmul10add 11916 4t3lem 11944 9t11e99 11977 decbin2 11988 binom2i 13293 3dec 13371 faclbnd4lem1 13398 3dvds2dec 15461 mod2xnegi 16179 decsplit 16191 log2ublem1 25125 log2ublem2 25126 bposlem8 25468 ax5seglem7 26284 ip0i 28266 ip1ilem 28267 ipasslem10 28280 normlem0 28552 polid2i 28600 lnopunilem1 29455 dfdec100 30154 dpmul10 30179 dpmul 30197 dpmul4 30198 sqmid3api 38141 fourierswlem 41366 3exp4mod41 42546 2t6m3t4e0 43133 |
Copyright terms: Public domain | W3C validator |