![]() |
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 11206, for naming consistency with mulassi 11257. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulass 11206 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 (class class class)co 7419 ℂcc 11138 · cmul 11145 |
This theorem was proved from axioms: ax-mulass 11206 |
This theorem is referenced by: mulrid 11244 mulassi 11257 mulassd 11269 mul12 11411 mul32 11412 mul31 11413 mul4 11414 00id 11421 divass 11923 cju 12241 div4p1lem1div2 12500 xmulasslem3 13300 mulbinom2 14221 sqoddm1div8 14241 faclbnd5 14293 bcval5 14313 remim 15100 imval2 15134 01sqrexlem7 15231 sqrtneglem 15249 sqreulem 15342 clim2div 15871 prodfmul 15872 prodmolem3 15913 sinhval 16134 coshval 16135 absefib 16178 efieq1re 16179 muldvds1 16261 muldvds2 16262 dvdsmulc 16264 dvdsmulcr 16266 dvdstr 16274 eulerthlem2 16754 oddprmdvds 16875 ablfacrp 20035 cncrng 21333 cncrngOLD 21334 nmoleub2lem3 25086 cnlmod 25111 itg2mulc 25721 abssinper 26500 sinasin 26866 dchrabl 27232 bposlem6 27267 bposlem9 27270 2sqlem6 27401 rpvmasum2 27490 cncvcOLD 30465 ipasslem5 30717 ipasslem11 30722 dvasin 37305 facp2 41743 fac2xp3 41822 pellexlem2 42389 jm2.25 42559 expgrowth 43911 2zrngmsgrp 47498 nn0sumshdiglemA 47875 |
Copyright terms: Public domain | W3C validator |