Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adddi | GIF version |
Description: Alias for ax-distr 7717, for naming consistency with adddii 7769. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7717 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 = wceq 1331 ∈ wcel 1480 (class class class)co 5767 ℂcc 7611 + caddc 7616 · cmul 7618 |
This theorem was proved from axioms: ax-distr 7717 |
This theorem is referenced by: adddir 7750 adddii 7769 adddid 7783 muladd11 7888 cnegex 7933 muladd 8139 nnmulcl 8734 expmul 10331 bernneq 10405 sqoddm1div8 10437 isermulc2 11102 efexp 11377 efi4p 11413 sinadd 11432 cosadd 11433 cos2tsin 11447 cos01bnd 11454 absefib 11466 efieq1re 11467 demoivreALT 11469 odd2np1 11559 opoe 11581 opeo 11583 gcdmultiple 11697 sinperlem 12878 |
Copyright terms: Public domain | W3C validator |