![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddi | GIF version |
Description: Alias for ax-distr 7748, for naming consistency with adddii 7800. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7748 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 963 = wceq 1332 ∈ wcel 1481 (class class class)co 5782 ℂcc 7642 + caddc 7647 · cmul 7649 |
This theorem was proved from axioms: ax-distr 7748 |
This theorem is referenced by: adddir 7781 adddii 7800 adddid 7814 muladd11 7919 cnegex 7964 muladd 8170 nnmulcl 8765 expmul 10369 bernneq 10443 sqoddm1div8 10475 isermulc2 11141 efexp 11425 efi4p 11460 sinadd 11479 cosadd 11480 cos2tsin 11494 cos01bnd 11501 absefib 11513 efieq1re 11514 demoivreALT 11516 odd2np1 11606 opoe 11628 opeo 11630 gcdmultiple 11744 sinperlem 12937 |
Copyright terms: Public domain | W3C validator |