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 10614 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1452 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 10592 |
This theorem depends on definitions: df-bi 208 df-an 397 df-3an 1081 |
This theorem is referenced by: addid1 10808 3t3e9 11792 numltc 12112 numsucc 12126 numma 12130 decmul10add 12155 4t3lem 12183 9t11e99 12216 decbin2 12227 binom2i 13562 3dec 13614 faclbnd4lem1 13641 3dvds2dec 15670 mod2xnegi 16395 decsplit 16407 log2ublem1 25451 log2ublem2 25452 bposlem8 25794 ax5seglem7 26648 ip0i 28529 ip1ilem 28530 ipasslem10 28543 normlem0 28813 polid2i 28861 lnopunilem1 29714 dfdec100 30473 dpmul10 30498 dpmul 30516 dpmul4 30517 sn-1ne2 39036 sqmid3api 39047 fourierswlem 42392 3exp4mod41 43658 2t6m3t4e0 44324 |
Copyright terms: Public domain | W3C validator |