| 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 11222, for naming consistency with adddii 11273. (Contributed by NM, 10-Mar-2008.) |
| Ref | Expression |
|---|---|
| adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-distr 11222 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 + caddc 11158 · cmul 11160 |
| This theorem was proved from axioms: ax-distr 11222 |
| This theorem is referenced by: adddir 11252 adddii 11273 adddid 11285 muladd11 11431 mul02lem1 11437 mul02 11439 muladd 11695 nnmulcl 12290 xadddilem 13336 expmul 14148 bernneq 14268 sqoddm1div8 14282 sqreulem 15398 isermulc2 15694 fsummulc2 15820 fsumcube 16096 efexp 16137 efi4p 16173 sinadd 16200 cosadd 16201 cos2tsin 16215 cos01bnd 16222 absefib 16234 efieq1re 16235 demoivreALT 16237 odd2np1 16378 opoe 16400 opeo 16402 pythagtriplem12 16864 cncrng 21401 cncrngOLD 21402 cnlmod 25173 plydivlem4 26338 sinperlem 26522 cxpsqrt 26745 chtub 27256 bcp1ctr 27323 2lgslem3d1 27447 cncvcOLD 30602 hhph 31197 2zrngALT 48170 |
| Copyright terms: Public domain | W3C validator |