![]() |
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 10493 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1491 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 (class class class)co 6878 ℂcc 10222 · cmul 10229 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-mulcom 10288 ax-mulass 10290 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-iota 6064 df-fv 6109 df-ov 6881 |
This theorem is referenced by: conjmul 11034 modmul1 12978 binom3 13239 bernneq 13244 expmulnbnd 13250 discr 13255 bcm1k 13355 bcp1n 13356 reccn2 14668 binomlem 14899 binomfallfaclem2 15107 tanadd 15233 eirrlem 15268 dvds2ln 15353 bezoutlem4 15594 divgcdcoprm0 15713 modprm0 15843 nrginvrcnlem 22823 tcphcphlem2 23362 csbren 23521 radcnvlem1 24508 tanarg 24706 cxpeq 24842 quad2 24918 binom4 24929 dquartlem2 24931 dquart 24932 quart1lem 24934 dvatan 25014 log2cnv 25023 basellem8 25166 bcmono 25354 gausslemma2d 25451 lgsquadlem1 25457 2lgslem3b 25474 2lgslem3c 25475 2lgslem3d 25476 rplogsumlem1 25525 dchrisumlem2 25531 chpdifbndlem1 25594 selberg3lem1 25598 selberg4 25602 selberg3r 25610 pntrlog2bndlem2 25619 pntrlog2bndlem3 25620 pntrlog2bndlem5 25622 pntlemf 25646 pntlemo 25648 ostth2lem1 25659 ostth2lem3 25676 logdivsqrle 31248 circum 32083 jm2.25 38347 jm2.27c 38355 binomcxplemnotnn0 39333 dvasinbx 40875 stirlinglem3 41032 dirkercncflem2 41060 cevathlem1 41798 |
Copyright terms: Public domain | W3C validator |