![]() |
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 11144 | . . . 4 โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) | |
2 | 1 | oveq1d 7377 | . . 3 โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ)) |
3 | 2 | 3adant3 1133 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ต ยท ๐ด) ยท ๐ถ)) |
4 | mulass 11146 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) | |
5 | mulass 11146 | . . 3 โข ((๐ต โ โ โง ๐ด โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ))) | |
6 | 5 | 3com12 1124 | . 2 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ด) ยท ๐ถ) = (๐ต ยท (๐ด ยท ๐ถ))) |
7 | 3, 4, 6 | 3eqtr3d 2785 | 1 โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต ยท ๐ถ)) = (๐ต ยท (๐ด ยท ๐ถ))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 397 โง w3a 1088 = wceq 1542 โ wcel 2107 (class class class)co 7362 โcc 11056 ยท cmul 11063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-mulcom 11122 ax-mulass 11124 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-iota 6453 df-fv 6509 df-ov 7365 |
This theorem is referenced by: mul02 11340 mul12i 11357 mul12d 11371 mulre 15013 sqreulem 15251 fsumcube 15950 demoivre 16089 demoivreALT 16090 dvdscmul 16172 dvdscmulr 16174 dvdstr 16183 ablfacrp 19852 nmoleub2lem3 24494 sinperlem 25853 coskpi 25895 sineq0 25896 efif1olem4 25917 rpvmasum2 26876 expgrowthi 42687 |
Copyright terms: Public domain | W3C validator |