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 10891 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1459 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2108 (class class class)co 7255 ℂcc 10800 + caddc 10805 · cmul 10807 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 10869 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1087 |
This theorem is referenced by: addid1 11085 3t3e9 12070 numltc 12392 numsucc 12406 numma 12410 decmul10add 12435 4t3lem 12463 9t11e99 12496 decbin2 12507 binom2i 13856 3dec 13908 faclbnd4lem1 13935 3dvds2dec 15970 mod2xnegi 16700 decsplit 16712 log2ublem1 26001 log2ublem2 26002 bposlem8 26344 ax5seglem7 27206 ip0i 29088 ip1ilem 29089 ipasslem10 29102 normlem0 29372 polid2i 29420 lnopunilem1 30273 dfdec100 31046 dpmul10 31071 dpmul 31089 dpmul4 31090 sn-1ne2 40216 sqmid3api 40232 ipiiie0 40340 sn-0tie0 40342 fourierswlem 43661 3exp4mod41 44956 2t6m3t4e0 45572 |
Copyright terms: Public domain | W3C validator |