Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mul12d | Structured version Visualization version GIF version |
Description: Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcomd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addcand.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
mul12d | ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcomd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcand.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | mul12 10202 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1326 | 1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ∈ wcel 1990 (class class class)co 6650 ℂcc 9934 · cmul 9941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-mulcom 10000 ax-mulass 10002 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 |
This theorem is referenced by: divrec 10701 remullem 13868 sqreulem 14099 cvgrat 14615 binomrisefac 14773 tanval3 14864 sinadd 14894 dvdsmulgcd 15274 lcmgcdlem 15319 cncongr1 15381 prmdiv 15490 vdwlem6 15690 itgmulc2 23600 dvexp3 23741 aaliou3lem8 24100 dvradcnv 24175 pserdvlem2 24182 abelthlem6 24190 abelthlem7 24192 tangtx 24257 tanarg 24365 dvcxp1 24481 dvcncxp1 24484 heron 24565 dcubic1 24572 mcubic 24574 dquart 24580 quart1 24583 quartlem1 24584 asinsin 24619 lgamgulmlem2 24756 basellem3 24809 bcp1ctr 25004 gausslemma2dlem6 25097 lgseisenlem2 25101 lgseisenlem4 25103 lgsquadlem1 25105 2sqlem4 25146 chebbnd1lem3 25160 rpvmasum2 25201 mulog2sumlem3 25225 selberglem1 25234 selberg4lem1 25249 selberg3r 25258 selberg34r 25260 pntrlog2bndlem4 25269 pntrlog2bndlem6 25272 pntlemr 25291 pntlemk 25295 ostth2lem3 25324 colinearalglem4 25789 branmfn 28964 vtsprod 30717 hgt750leme 30736 faclimlem1 31629 itgmulc2nc 33478 areacirclem1 33500 pellexlem6 37398 pell1234qrmulcl 37419 rmxyadd 37486 jm2.18 37555 jm2.19lem1 37556 jm2.22 37562 jm2.20nn 37564 proot1ex 37779 ofmul12 38524 binomcxplemnotnn0 38555 sineq0ALT 39173 mul13d 39491 stoweidlem11 40228 wallispi2lem1 40288 stirlinglem1 40291 stirlinglem3 40293 stirlinglem7 40297 stirlinglem15 40305 dirkertrigeqlem3 40317 dirkercncflem2 40321 fourierdlem66 40389 fourierdlem83 40406 etransclem23 40474 mod42tp1mod8 41519 2zlidl 41934 |
Copyright terms: Public domain | W3C validator |