| 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 11244 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
| 5 | 1, 2, 3, 4 | mp3an 1463 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 + caddc 11158 · cmul 11160 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 11222 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: addrid 11441 3t3e9 12433 numltc 12759 numsucc 12773 numma 12777 decmul10add 12802 4t3lem 12830 9t11e99 12863 decbin2 12874 binom2i 14251 3dec 14305 faclbnd4lem1 14332 3dvds2dec 16370 mod2xnegi 17109 decsplit 17120 log2ublem1 26989 log2ublem2 26990 bposlem8 27335 ax5seglem7 28950 ip0i 30844 ip1ilem 30845 ipasslem10 30858 normlem0 31128 polid2i 31176 lnopunilem1 32029 dfdec100 32832 dpmul10 32877 dpmul 32895 dpmul4 32896 sn-1ne2 42300 sqmid3api 42318 ipiiie0 42467 sn-0tie0 42469 fourierswlem 46245 3exp4mod41 47603 2t6m3t4e0 48264 |
| Copyright terms: Public domain | W3C validator |