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 10081 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1318 | 1 ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 (class class class)co 6549 ℂcc 9813 · cmul 9820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-mulcom 9879 ax-mulass 9881 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 |
This theorem is referenced by: divrec 10580 remullem 13716 sqreulem 13947 cvgrat 14454 binomrisefac 14612 tanval3 14703 sinadd 14733 dvdsmulgcd 15112 lcmgcdlem 15157 cncongr1 15219 prmdiv 15328 vdwlem6 15528 itgmulc2 23406 dvexp3 23545 aaliou3lem8 23904 dvradcnv 23979 pserdvlem2 23986 abelthlem6 23994 abelthlem7 23996 tangtx 24061 tanarg 24169 dvcxp1 24281 dvcncxp1 24284 heron 24365 dcubic1 24372 mcubic 24374 dquart 24380 quart1 24383 quartlem1 24384 asinsin 24419 lgamgulmlem2 24556 basellem3 24609 bcp1ctr 24804 gausslemma2dlem6 24897 lgseisenlem2 24901 lgseisenlem4 24903 lgsquadlem1 24905 2sqlem4 24946 chebbnd1lem3 24960 rpvmasum2 25001 mulog2sumlem3 25025 selberglem1 25034 selberg4lem1 25049 selberg3r 25058 selberg34r 25060 pntrlog2bndlem4 25069 pntrlog2bndlem6 25072 pntlemr 25091 pntlemk 25095 ostth2lem3 25124 colinearalglem4 25589 branmfn 28348 faclimlem1 30882 itgmulc2nc 32648 areacirclem1 32670 pellexlem6 36416 pell1234qrmulcl 36437 rmxyadd 36504 jm2.18 36573 jm2.19lem1 36574 jm2.22 36580 jm2.20nn 36582 proot1ex 36798 ofmul12 37546 binomcxplemnotnn0 37577 sineq0ALT 38195 mul13d 38432 stoweidlem11 38904 wallispi2lem1 38964 stirlinglem1 38967 stirlinglem3 38969 stirlinglem7 38973 stirlinglem15 38981 dirkertrigeqlem3 38993 dirkercncflem2 38997 fourierdlem66 39065 fourierdlem83 39082 etransclem23 39150 mod42tp1mod8 40057 2zlidl 41724 |
Copyright terms: Public domain | W3C validator |