![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adddi | GIF version |
Description: Alias for ax-distr 7944, for naming consistency with adddii 7996. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
adddi | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-distr 7944 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 = wceq 1364 ∈ wcel 2160 (class class class)co 5895 ℂcc 7838 + caddc 7843 · cmul 7845 |
This theorem was proved from axioms: ax-distr 7944 |
This theorem is referenced by: adddir 7977 adddii 7996 adddid 8011 muladd11 8119 cnegex 8164 muladd 8370 nnmulcl 8969 expmul 10595 bernneq 10671 sqoddm1div8 10704 isermulc2 11379 efexp 11721 efi4p 11756 sinadd 11775 cosadd 11776 cos2tsin 11790 cos01bnd 11797 absefib 11809 efieq1re 11810 demoivreALT 11812 odd2np1 11909 opoe 11931 opeo 11933 gcdmultiple 12052 pythagtriplem12 12306 cncrng 13869 sinperlem 14681 |
Copyright terms: Public domain | W3C validator |