![]() |
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 11227 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1458 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 (class class class)co 7420 ℂcc 11136 + caddc 11141 · cmul 11143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 11205 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1087 |
This theorem is referenced by: addrid 11424 3t3e9 12409 numltc 12733 numsucc 12747 numma 12751 decmul10add 12776 4t3lem 12804 9t11e99 12837 decbin2 12848 binom2i 14207 3dec 14257 faclbnd4lem1 14284 3dvds2dec 16309 mod2xnegi 17039 decsplit 17051 log2ublem1 26877 log2ublem2 26878 bposlem8 27223 ax5seglem7 28745 ip0i 30634 ip1ilem 30635 ipasslem10 30648 normlem0 30918 polid2i 30966 lnopunilem1 31819 dfdec100 32593 dpmul10 32618 dpmul 32636 dpmul4 32637 sn-1ne2 41840 sqmid3api 41857 ipiiie0 41992 sn-0tie0 41994 fourierswlem 45618 3exp4mod41 46956 2t6m3t4e0 47412 |
Copyright terms: Public domain | W3C validator |