|   | 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 11428 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | |
| 5 | 1, 2, 3, 4 | syl3anc 1372 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 (class class class)co 7432 ℂcc 11154 · cmul 11161 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-mulcom 11220 ax-mulass 11222 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-iota 6513 df-fv 6568 df-ov 7435 | 
| This theorem is referenced by: conjmul 11985 modmul1 13966 binom3 14264 bernneq 14269 expmulnbnd 14275 discr 14280 bcm1k 14355 bcp1n 14356 reccn2 15634 binomlem 15866 binomfallfaclem2 16077 tanadd 16204 eirrlem 16241 dvds2ln 16327 bezoutlem4 16580 divgcdcoprm0 16703 modprm0 16844 nrginvrcnlem 24713 tcphcphlem2 25271 csbren 25434 radcnvlem1 26457 tanarg 26662 cxpeq 26801 quad2 26883 binom4 26894 dquartlem2 26896 dquart 26897 quart1lem 26899 dvatan 26979 log2cnv 26988 basellem8 27132 bcmono 27322 gausslemma2d 27419 lgsquadlem1 27425 2lgslem3b 27442 2lgslem3c 27443 2lgslem3d 27444 rplogsumlem1 27529 dchrisumlem2 27535 chpdifbndlem1 27598 selberg3lem1 27602 selberg4 27606 selberg3r 27614 pntrlog2bndlem2 27623 pntrlog2bndlem3 27624 pntrlog2bndlem5 27626 pntlemf 27650 pntlemo 27652 ostth2lem1 27663 ostth2lem3 27680 zringfrac 33583 constrrtcc 33777 logdivsqrle 34666 circum 35680 lcmineqlem8 42038 lcmineqlem12 42042 flt4lem5f 42672 jm2.25 43016 jm2.27c 43024 binomcxplemnotnn0 44380 dvasinbx 45940 stirlinglem3 46096 dirkercncflem2 46124 cevathlem1 46887 itschlc0yqe 48686 | 
| Copyright terms: Public domain | W3C validator |