![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mul12 | Structured version Visualization version GIF version |
Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.) |
Ref | Expression |
---|---|
mul12 | โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulcom 11224 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) | |
2 | 1 | oveq1d 7435 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ)) |
3 | 2 | 3adant3 1130 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ)) |
4 | mulass 11226 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) | |
5 | mulass 11226 | . . 3 โข ((๐ต โ โ โง ๐ด โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ))) | |
6 | 5 | 3com12 1121 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ))) |
7 | 3, 4, 6 | 3eqtr3d 2776 | 1 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 395 โง w3a 1085 = wceq 1534 โ wcel 2099 (class class class)co 7420 โcc 11136 ยท cmul 11143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-mulcom 11202 ax-mulass 11204 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 |
This theorem is referenced by: mul02 11422 mul12i 11439 mul12d 11453 mulre 15100 sqreulem 15338 fsumcube 16036 demoivre 16176 demoivreALT 16177 dvdscmul 16259 dvdscmulr 16261 dvdstr 16270 ablfacrp 20022 nmoleub2lem3 25041 sinperlem 26414 coskpi 26456 sineq0 26457 efif1olem4 26478 rpvmasum2 27444 expgrowthi 43770 |
Copyright terms: Public domain | W3C validator |