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 10025 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1424 | 1 ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ∈ wcel 1990 (class class class)co 6650 ℂcc 9934 + caddc 9939 · cmul 9941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-distr 10003 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: addid1 10216 3t3e9 11180 numltc 11528 numsucc 11549 numma 11557 decmul10add 11593 decmul10addOLD 11594 4t3lem 11631 9t11e99 11671 9t11e99OLD 11672 decbin2 11683 binom2i 12974 3dec 13050 3decOLD 13053 faclbnd4lem1 13080 3dvds2dec 15056 3dvds2decOLD 15057 mod2xnegi 15775 decsplit 15787 decsplitOLD 15791 log2ublem1 24673 log2ublem2 24674 bposlem8 25016 ax5seglem7 25815 ip0i 27680 ip1ilem 27681 ipasslem10 27694 normlem0 27966 polid2i 28014 lnopunilem1 28869 dfdec100 29576 dpmul10 29603 dpmul 29621 dpmul4 29622 fourierswlem 40447 3exp4mod41 41533 2t6m3t4e0 42126 |
Copyright terms: Public domain | W3C validator |