Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulass | GIF version |
Description: Alias for ax-mulass 7691, for naming consistency with mulassi 7743. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 7691 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 = wceq 1316 ∈ wcel 1465 (class class class)co 5742 ℂcc 7586 · cmul 7593 |
This theorem was proved from axioms: ax-mulass 7691 |
This theorem is referenced by: mulid1 7731 mulassi 7743 mulassd 7757 mul12 7859 mul32 7860 mul31 7861 mul4 7862 rimul 8315 divassap 8418 cju 8687 div4p1lem1div2 8941 mulbinom2 10376 sqoddm1div8 10412 remim 10600 imval2 10634 absefib 11404 efieq1re 11405 muldvds1 11445 muldvds2 11446 dvdsmulc 11448 dvdstr 11457 abssinper 12854 |
Copyright terms: Public domain | W3C validator |