|   | 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 11222, for naming consistency with mulassi 11273. (Contributed by NM, 10-Mar-2008.) | 
| Ref | Expression | 
|---|---|
| mulass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ax-mulass 11222 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 (class class class)co 7432 ℂcc 11154 · cmul 11161 | 
| This theorem was proved from axioms: ax-mulass 11222 | 
| This theorem is referenced by: mulrid 11260 mulassi 11273 mulassd 11285 mul12 11427 mul32 11428 mul31 11429 mul4 11430 00id 11437 divass 11941 cju 12263 div4p1lem1div2 12523 xmulasslem3 13329 mulbinom2 14263 sqoddm1div8 14283 faclbnd5 14338 bcval5 14358 remim 15157 imval2 15191 01sqrexlem7 15288 sqrtneglem 15306 sqreulem 15399 clim2div 15926 prodfmul 15927 prodmolem3 15970 sinhval 16191 coshval 16192 absefib 16235 efieq1re 16236 muldvds1 16319 muldvds2 16320 dvdsmulc 16322 dvdsmulcr 16324 dvdstr 16332 eulerthlem2 16820 oddprmdvds 16942 ablfacrp 20087 cncrng 21402 cncrngOLD 21403 nmoleub2lem3 25149 cnlmod 25174 itg2mulc 25783 abssinper 26564 sinasin 26933 dchrabl 27299 bposlem6 27334 bposlem9 27337 2sqlem6 27468 rpvmasum2 27557 cncvcOLD 30603 ipasslem5 30855 ipasslem11 30860 dvasin 37712 facp2 42145 fac2xp3 42241 pellexlem2 42846 jm2.25 43016 expgrowth 44359 2zrngmsgrp 48174 nn0sumshdiglemA 48545 | 
| Copyright terms: Public domain | W3C validator |