![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulass | Structured version Visualization version GIF version |
Description: Alias for ax-mulass 10040, for naming consistency with mulassi 10087. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 10040 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1054 = wceq 1523 ∈ wcel 2030 (class class class)co 6690 ℂcc 9972 · cmul 9979 |
This theorem was proved from axioms: ax-mulass 10040 |
This theorem is referenced by: mulid1 10075 mulassi 10087 mulassd 10101 mul12 10240 mul32 10241 mul31 10242 mul4 10243 00id 10249 divass 10741 cju 11054 div4p1lem1div2 11325 xmulasslem3 12154 mulbinom2 13024 sqoddm1div8 13068 faclbnd5 13125 bcval5 13145 remim 13901 imval2 13935 sqrlem7 14033 sqrtneglem 14051 sqreulem 14143 clim2div 14665 prodfmul 14666 prodmolem3 14707 sinhval 14928 coshval 14929 absefib 14972 efieq1re 14973 muldvds1 15053 muldvds2 15054 dvdsmulc 15056 dvdsmulcr 15058 dvdstr 15065 eulerthlem2 15534 oddprmdvds 15654 ablfacrp 18511 cncrng 19815 nmoleub2lem3 22961 cnlmod 22986 itg2mulc 23559 abssinper 24315 sinasin 24661 dchrabl 25024 bposlem6 25059 bposlem9 25062 lgsdir 25102 lgsdi 25104 2sqlem6 25193 rpvmasum2 25246 cncvcOLD 27566 ipasslem5 27818 ipasslem11 27823 dvasin 33626 pellexlem2 37711 jm2.25 37883 expgrowth 38851 2zrngmsgrp 42272 nn0sumshdiglemA 42738 |
Copyright terms: Public domain | W3C validator |