![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mul4d | Structured version Visualization version GIF version |
Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcomd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addcand.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
mul4d.4 | ⊢ (𝜑 → 𝐷 ∈ ℂ) |
Ref | Expression |
---|---|
mul4d | ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcomd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcand.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | mul4d.4 | . 2 ⊢ (𝜑 → 𝐷 ∈ ℂ) | |
5 | mul4 11420 | . 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | |
6 | 1, 2, 3, 4, 5 | syl22anc 837 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 (class class class)co 7426 ℂcc 11144 · cmul 11151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 ax-mulcl 11208 ax-mulcom 11210 ax-mulass 11212 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-iota 6505 df-fv 6561 df-ov 7429 |
This theorem is referenced by: remullem 15115 absmul 15281 binomrisefac 16026 cosadd 16149 tanadd 16151 eulerthlem2 16758 mul4sqlem 16929 odadd2 19811 itgmulc2 25783 plymullem1 26168 chordthmlem4 26787 heron 26790 quartlem1 26809 dchrmulcl 27202 bposlem9 27245 lgsdir 27285 lgsdi 27287 lgsquad2lem1 27337 chtppilimlem1 27426 rplogsumlem1 27437 dchrvmasumlem1 27448 dchrvmasum2lem 27449 chpdifbndlem1 27506 pntlemf 27558 brbtwn2 28736 colinearalglem4 28740 zringfrac 33277 madjusmdetlem4 33464 hgt750lemf 34318 hgt750leme 34323 circum 35311 itgmulc2nc 37194 flt4lem5e 42111 pellexlem6 42285 pell1234qrmulcl 42306 rmxyadd 42373 wallispi2lem2 45489 dirkertrigeqlem3 45517 cevathlem1 46284 itsclc0xyqsolr 47920 |
Copyright terms: Public domain | W3C validator |