|   | 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 11429 | . 2 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | |
| 6 | 1, 2, 3, 4, 5 | syl22anc 839 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 · cmul 11160 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-mulcl 11217 ax-mulcom 11219 ax-mulass 11221 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 | 
| This theorem is referenced by: remullem 15167 absmul 15333 binomrisefac 16078 cosadd 16201 tanadd 16203 eulerthlem2 16819 mul4sqlem 16991 odadd2 19867 itgmulc2 25869 plymullem1 26253 chordthmlem4 26878 heron 26881 quartlem1 26900 dchrmulcl 27293 bposlem9 27336 lgsdir 27376 lgsdi 27378 lgsquad2lem1 27428 chtppilimlem1 27517 rplogsumlem1 27528 dchrvmasumlem1 27539 dchrvmasum2lem 27540 chpdifbndlem1 27597 pntlemf 27649 brbtwn2 28920 colinearalglem4 28924 zringfrac 33582 madjusmdetlem4 33829 hgt750lemf 34668 hgt750leme 34673 circum 35679 itgmulc2nc 37695 flt4lem5e 42666 pellexlem6 42845 pell1234qrmulcl 42866 rmxyadd 42933 wallispi2lem2 46087 dirkertrigeqlem3 46115 cevathlem1 46882 itsclc0xyqsolr 48690 | 
| Copyright terms: Public domain | W3C validator |