![]() |
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 10399, for naming consistency with mulassi 10449. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 10399 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 (class class class)co 6974 ℂcc 10331 · cmul 10338 |
This theorem was proved from axioms: ax-mulass 10399 |
This theorem is referenced by: mulid1 10435 mulassi 10449 mulassd 10461 mul12 10603 mul32 10604 mul31 10605 mul4 10606 00id 10613 divass 11115 cju 11433 div4p1lem1div2 11700 xmulasslem3 12493 mulbinom2 13397 sqoddm1div8 13417 faclbnd5 13471 bcval5 13491 remim 14335 imval2 14369 sqrlem7 14467 sqrtneglem 14485 sqreulem 14578 clim2div 15103 prodfmul 15104 prodmolem3 15145 sinhval 15365 coshval 15366 absefib 15409 efieq1re 15410 muldvds1 15492 muldvds2 15493 dvdsmulc 15495 dvdsmulcr 15497 dvdstr 15504 eulerthlem2 15973 oddprmdvds 16093 ablfacrp 18950 cncrng 20280 nmoleub2lem3 23434 cnlmod 23459 itg2mulc 24063 abssinper 24821 sinasin 25180 dchrabl 25544 bposlem6 25579 bposlem9 25582 2sqlem6 25713 rpvmasum2 25802 cncvcOLD 28149 ipasslem5 28401 ipasslem11 28406 dvasin 34448 pellexlem2 38852 jm2.25 39021 expgrowth 40112 2zrngmsgrp 43607 nn0sumshdiglemA 44072 |
Copyright terms: Public domain | W3C validator |