![]() |
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 11255 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1372 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 (class class class)co 7350 ℂcc 10983 · cmul 10990 |
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 2709 ax-mulcom 11049 ax-mulass 11051 |
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 2716 df-cleq 2730 df-clel 2816 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-iota 6444 df-fv 6500 df-ov 7353 |
This theorem is referenced by: conjmul 11806 modmul1 13759 binom3 14054 bernneq 14059 expmulnbnd 14065 discr 14070 bcm1k 14144 bcp1n 14145 reccn2 15415 binomlem 15650 binomfallfaclem2 15859 tanadd 15985 eirrlem 16022 dvds2ln 16107 bezoutlem4 16359 divgcdcoprm0 16477 modprm0 16613 nrginvrcnlem 23983 tcphcphlem2 24528 csbren 24691 radcnvlem1 25700 tanarg 25902 cxpeq 26038 quad2 26117 binom4 26128 dquartlem2 26130 dquart 26131 quart1lem 26133 dvatan 26213 log2cnv 26222 basellem8 26365 bcmono 26553 gausslemma2d 26650 lgsquadlem1 26656 2lgslem3b 26673 2lgslem3c 26674 2lgslem3d 26675 rplogsumlem1 26760 dchrisumlem2 26766 chpdifbndlem1 26829 selberg3lem1 26833 selberg4 26837 selberg3r 26845 pntrlog2bndlem2 26854 pntrlog2bndlem3 26855 pntrlog2bndlem5 26857 pntlemf 26881 pntlemo 26883 ostth2lem1 26894 ostth2lem3 26911 logdivsqrle 33043 circum 34044 lcmineqlem8 40424 lcmineqlem12 40428 flt4lem5f 40897 jm2.25 41225 jm2.27c 41233 binomcxplemnotnn0 42437 dvasinbx 43952 stirlinglem3 44108 dirkercncflem2 44136 cevathlem1 44899 itschlc0yqe 46637 |
Copyright terms: Public domain | W3C validator |