![]() |
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 11430 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | |
5 | 1, 2, 3, 4 | syl3anc 1368 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 (class class class)co 7424 ℂcc 11156 · cmul 11163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-mulcom 11222 ax-mulass 11224 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 df-ov 7427 |
This theorem is referenced by: conjmul 11982 modmul1 13944 binom3 14241 bernneq 14246 expmulnbnd 14252 discr 14257 bcm1k 14332 bcp1n 14333 reccn2 15599 binomlem 15833 binomfallfaclem2 16042 tanadd 16169 eirrlem 16206 dvds2ln 16291 bezoutlem4 16543 divgcdcoprm0 16666 modprm0 16807 nrginvrcnlem 24699 tcphcphlem2 25255 csbren 25418 radcnvlem1 26442 tanarg 26646 cxpeq 26785 quad2 26867 binom4 26878 dquartlem2 26880 dquart 26881 quart1lem 26883 dvatan 26963 log2cnv 26972 basellem8 27116 bcmono 27306 gausslemma2d 27403 lgsquadlem1 27409 2lgslem3b 27426 2lgslem3c 27427 2lgslem3d 27428 rplogsumlem1 27513 dchrisumlem2 27519 chpdifbndlem1 27582 selberg3lem1 27586 selberg4 27590 selberg3r 27598 pntrlog2bndlem2 27607 pntrlog2bndlem3 27608 pntrlog2bndlem5 27610 pntlemf 27634 pntlemo 27636 ostth2lem1 27647 ostth2lem3 27664 zringfrac 33429 logdivsqrle 34496 circum 35502 lcmineqlem8 41735 lcmineqlem12 41739 flt4lem5f 42311 jm2.25 42657 jm2.27c 42665 binomcxplemnotnn0 44030 dvasinbx 45541 stirlinglem3 45697 dirkercncflem2 45725 cevathlem1 46488 itschlc0yqe 48148 |
Copyright terms: Public domain | W3C validator |