| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mulcom | Structured version Visualization version GIF version | ||
| Description: Alias for ax-mulcom 11219, for naming consistency with mulcomi 11269. (Contributed by NM, 10-Mar-2008.) |
| Ref | Expression |
|---|---|
| mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-mulcom 11219 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 · cmul 11160 |
| This theorem was proved from axioms: ax-mulcom 11219 |
| This theorem is referenced by: adddir 11252 mullid 11260 mulcomi 11269 mulcomd 11282 mul12 11426 mul32 11427 mul31 11428 mul4r 11430 mul01 11440 muladd 11695 subdir 11697 mulneg2 11700 recextlem1 11893 mulcan2g 11917 divmul3 11927 div23 11941 div13 11943 div12 11944 divmulasscom 11946 divcan4 11949 divmul13 11970 divmul24 11971 divcan7 11976 div2neg 11990 prodgt02 12115 ltmul2 12118 lemul2 12120 lemul2a 12122 ltmulgt12 12128 lemulge12 12131 ltmuldiv2 12142 ltdivmul2 12145 lt2mul2div 12146 ledivmul2 12147 lemuldiv2 12149 supmul 12240 times2 12403 modcyc 13946 modcyc2 13947 modmulmodr 13978 subsq 14249 cjmulrcl 15183 imval2 15190 abscj 15318 sqabsadd 15321 sqabssub 15322 sqreulem 15398 iseraltlem2 15719 iseraltlem3 15720 climcndslem2 15886 prodfmul 15926 prodmolem3 15969 bpoly3 16094 efcllem 16113 efexp 16137 sinmul 16208 demoivreALT 16237 dvdsmul1 16315 odd2np1lem 16377 odd2np1 16378 opeo 16402 omeo 16403 modgcd 16569 bezoutlem1 16576 dvdsgcd 16581 coprmdvds 16690 coprmdvds2 16691 qredeq 16694 eulerthlem2 16819 modprm0 16843 modprmn0modprm0 16845 coprimeprodsq2 16847 prmreclem6 16959 odmod 19564 cncrng 21401 cncrngOLD 21402 cnsrng 21418 pcoass 25057 clmvscom 25123 dvlipcn 26033 plydivlem4 26338 quotcan 26351 aaliou3lem3 26386 ef2kpi 26520 sinperlem 26522 sinmpi 26529 cosmpi 26530 sinppi 26531 cosppi 26532 sineq0 26566 tanregt0 26581 logneg 26630 lognegb 26632 logimul 26656 tanarg 26661 logtayl 26702 cxpsqrtlem 26744 cxpcom 26781 cubic2 26891 quart1 26899 log2cnv 26987 basellem1 27124 basellem3 27126 basellem5 27128 basellem8 27131 mumul 27224 chtublem 27255 perfectlem1 27273 perfectlem2 27274 perfect 27275 dchrabl 27298 bposlem6 27333 bposlem9 27336 lgsdir2lem4 27372 lgsdir2 27374 lgsquadlem2 27425 lgsquad2 27430 rpvmasum2 27556 mulog2sumlem1 27578 pntibndlem2 27635 pntibndlem3 27636 pntlemf 27649 nvscom 30648 ipasslem11 30859 ipblnfi 30874 hvmulcom 31062 h1de2bi 31573 homul12 31824 riesz3i 32081 riesz1 32084 kbass4 32138 sin2h 37617 heiborlem6 37823 rmym1 42947 expgrowthi 44352 expgrowth 44354 stoweidlem10 46025 perfectALTVlem1 47708 perfectALTVlem2 47709 perfectALTV 47710 tgoldbachlt 47803 2zrngnmlid2 48173 |
| Copyright terms: Public domain | W3C validator |