![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mul32d | Structured version Visualization version GIF version |
Description: Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcomd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addcand.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
mul32d | ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcomd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcand.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | mul32 10795 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1368 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 (class class class)co 7135 ℂcc 10524 · cmul 10531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-mulcom 10590 ax-mulass 10592 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 |
This theorem is referenced by: conjmul 11346 modmul1 13287 binom3 13581 bernneq 13586 expmulnbnd 13592 discr 13597 bcm1k 13671 bcp1n 13672 reccn2 14945 binomlem 15176 binomfallfaclem2 15386 tanadd 15512 eirrlem 15549 dvds2ln 15634 bezoutlem4 15880 divgcdcoprm0 15999 modprm0 16132 nrginvrcnlem 23297 tcphcphlem2 23840 csbren 24003 radcnvlem1 25008 tanarg 25210 cxpeq 25346 quad2 25425 binom4 25436 dquartlem2 25438 dquart 25439 quart1lem 25441 dvatan 25521 log2cnv 25530 basellem8 25673 bcmono 25861 gausslemma2d 25958 lgsquadlem1 25964 2lgslem3b 25981 2lgslem3c 25982 2lgslem3d 25983 rplogsumlem1 26068 dchrisumlem2 26074 chpdifbndlem1 26137 selberg3lem1 26141 selberg4 26145 selberg3r 26153 pntrlog2bndlem2 26162 pntrlog2bndlem3 26163 pntrlog2bndlem5 26165 pntlemf 26189 pntlemo 26191 ostth2lem1 26202 ostth2lem3 26219 logdivsqrle 32031 circum 33030 lcmineqlem8 39324 lcmineqlem12 39328 jm2.25 39940 jm2.27c 39948 binomcxplemnotnn0 41060 dvasinbx 42562 stirlinglem3 42718 dirkercncflem2 42746 cevathlem1 43481 itschlc0yqe 45174 |
Copyright terms: Public domain | W3C validator |