Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adddi | GIF version |
Description: Alias for ax-distr 7865, for naming consistency with adddii 7917. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7865 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 973 = wceq 1348 ∈ wcel 2141 (class class class)co 5850 ℂcc 7759 + caddc 7764 · cmul 7766 |
This theorem was proved from axioms: ax-distr 7865 |
This theorem is referenced by: adddir 7898 adddii 7917 adddid 7931 muladd11 8039 cnegex 8084 muladd 8290 nnmulcl 8886 expmul 10508 bernneq 10583 sqoddm1div8 10616 isermulc2 11290 efexp 11632 efi4p 11667 sinadd 11686 cosadd 11687 cos2tsin 11701 cos01bnd 11708 absefib 11720 efieq1re 11721 demoivreALT 11723 odd2np1 11819 opoe 11841 opeo 11843 gcdmultiple 11962 pythagtriplem12 12216 sinperlem 13482 |
Copyright terms: Public domain | W3C validator |