Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > adddi | Structured version Visualization version GIF version |
Description: Alias for ax-distr 10592, for naming consistency with adddii 10641. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 10592 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 · cmul 10530 |
This theorem was proved from axioms: ax-distr 10592 |
This theorem is referenced by: adddir 10620 adddii 10641 adddid 10653 muladd11 10798 mul02lem1 10804 mul02 10806 muladd 11060 nnmulcl 11649 xadddilem 12675 expmul 13462 bernneq 13578 sqoddm1div8 13592 sqreulem 14707 isermulc2 15002 fsummulc2 15127 fsumcube 15402 efexp 15442 efi4p 15478 sinadd 15505 cosadd 15506 cos2tsin 15520 cos01bnd 15527 absefib 15539 efieq1re 15540 demoivreALT 15542 odd2np1 15678 opoe 15700 opeo 15702 gcdmultipleOLD 15888 pythagtriplem12 16151 cncrng 20494 cnlmod 23671 plydivlem4 24812 sinperlem 24993 cxpsqrt 25213 chtub 25715 bcp1ctr 25782 2lgslem3d1 25906 cncvcOLD 28287 hhph 28882 2zrngALT 44147 |
Copyright terms: Public domain | W3C validator |