![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddi | GIF version |
Description: Alias for ax-distr 7512, for naming consistency with adddii 7561. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7512 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 925 = wceq 1290 ∈ wcel 1439 (class class class)co 5668 ℂcc 7411 + caddc 7416 · cmul 7418 |
This theorem was proved from axioms: ax-distr 7512 |
This theorem is referenced by: adddir 7542 adddii 7561 adddid 7575 muladd11 7678 cnegex 7723 muladd 7925 nnmulcl 8506 expmul 10063 bernneq 10137 sqoddm1div8 10169 iisermulc2 10791 efexp 11035 efi4p 11071 sinadd 11090 cosadd 11091 cos2tsin 11105 cos01bnd 11112 absefib 11123 efieq1re 11124 demoivreALT 11126 odd2np1 11214 opoe 11236 opeo 11238 gcdmultiple 11350 |
Copyright terms: Public domain | W3C validator |