![]() |
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 10212, for naming consistency with mulcomi 10258. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 10212 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2139 (class class class)co 6814 ℂcc 10146 · cmul 10153 |
This theorem was proved from axioms: ax-mulcom 10212 |
This theorem is referenced by: adddir 10243 mulid2 10250 mulcomi 10258 mulcomd 10273 mul12 10414 mul32 10415 mul31 10416 mul01 10427 muladd 10674 subdir 10676 mulneg2 10679 recextlem1 10869 mulcan2g 10893 divmul3 10902 div23 10916 div13 10918 div12 10919 divmulasscom 10921 divcan4 10924 divmul13 10940 divmul24 10941 divcan7 10946 div2neg 10960 prodgt02 11081 prodge02 11083 ltmul2 11086 lemul2 11088 lemul2a 11090 ltmulgt12 11096 lemulge12 11098 ltmuldiv2 11109 ltdivmul2 11112 lt2mul2div 11113 ledivmul2 11114 lemuldiv2 11116 supmul 11207 times2 11358 modcyc 12919 modcyc2 12920 modmulmodr 12950 subsq 13186 cjmulrcl 14103 imval2 14110 abscj 14238 sqabsadd 14241 sqabssub 14242 sqreulem 14318 iseraltlem2 14632 iseraltlem3 14633 climcndslem2 14801 prodfmul 14841 prodmolem3 14882 bpoly3 15008 efcllem 15027 efexp 15050 sinmul 15121 demoivreALT 15150 dvdsmul1 15225 odd2np1lem 15286 odd2np1 15287 opeo 15311 omeo 15312 modgcd 15475 bezoutlem1 15478 dvdsgcd 15483 gcdmultiple 15491 coprmdvds 15588 coprmdvdsOLD 15589 coprmdvds2 15590 qredeq 15593 eulerthlem2 15709 modprm0 15732 modprmn0modprm0 15734 coprimeprodsq2 15736 prmreclem6 15847 odmod 18185 cncrng 19989 cnsrng 20002 pcoass 23044 clmvscom 23110 dvlipcn 23976 plydivlem4 24270 quotcan 24283 aaliou3lem3 24318 ef2kpi 24450 sinperlem 24452 sinmpi 24459 cosmpi 24460 sinppi 24461 cosppi 24462 sineq0 24493 tanregt0 24505 logneg 24554 lognegb 24556 logimul 24580 tanarg 24585 logtayl 24626 cxpsqrtlem 24668 cubic2 24795 quart1 24803 log2cnv 24891 basellem1 25027 basellem3 25029 basellem5 25031 basellem8 25034 mumul 25127 chtublem 25156 perfectlem1 25174 perfectlem2 25175 perfect 25176 dchrabl 25199 bposlem6 25234 bposlem9 25237 lgsdir2lem4 25273 lgsdir2 25275 lgsdir 25277 lgsdi 25279 lgsquadlem2 25326 lgsquad2 25331 rpvmasum2 25421 mulog2sumlem1 25443 pntibndlem2 25500 pntibndlem3 25501 pntlemf 25514 nvscom 27814 ipasslem11 28025 ipblnfi 28041 hvmulcom 28230 h1de2bi 28743 homul12 28994 riesz3i 29251 riesz1 29254 kbass4 29308 sin2h 33730 heiborlem6 33946 rmym1 38020 expgrowthi 39052 expgrowth 39054 stoweidlem10 40748 perfectALTVlem1 42158 perfectALTVlem2 42159 perfectALTV 42160 tgoldbachlt 42232 tgoldbachltOLD 42238 2zrngnmlid2 42479 |
Copyright terms: Public domain | W3C validator |