![]() |
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 11218, for naming consistency with mulcomi 11268. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 11218 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 (class class class)co 7423 ℂcc 11152 · cmul 11159 |
This theorem was proved from axioms: ax-mulcom 11218 |
This theorem is referenced by: adddir 11251 mullid 11259 mulcomi 11268 mulcomd 11281 mul12 11425 mul32 11426 mul31 11427 mul4r 11429 mul01 11439 muladd 11692 subdir 11694 mulneg2 11697 recextlem1 11890 mulcan2g 11914 divmul3 11924 div23 11938 div13 11940 div12 11941 divmulasscom 11943 divcan4 11946 divmul13 11964 divmul24 11965 divcan7 11970 div2neg 11984 prodgt02 12109 ltmul2 12112 lemul2 12114 lemul2a 12116 ltmulgt12 12122 lemulge12 12124 ltmuldiv2 12135 ltdivmul2 12138 lt2mul2div 12139 ledivmul2 12140 lemuldiv2 12142 supmul 12233 times2 12396 modcyc 13921 modcyc2 13922 modmulmodr 13952 subsq 14223 cjmulrcl 15144 imval2 15151 abscj 15279 sqabsadd 15282 sqabssub 15283 sqreulem 15359 iseraltlem2 15682 iseraltlem3 15683 climcndslem2 15849 prodfmul 15889 prodmolem3 15930 bpoly3 16055 efcllem 16074 efexp 16098 sinmul 16169 demoivreALT 16198 dvdsmul1 16275 odd2np1lem 16337 odd2np1 16338 opeo 16362 omeo 16363 modgcd 16528 bezoutlem1 16535 dvdsgcd 16540 coprmdvds 16649 coprmdvds2 16650 qredeq 16653 eulerthlem2 16779 modprm0 16802 modprmn0modprm0 16804 coprimeprodsq2 16806 prmreclem6 16918 odmod 19539 cncrng 21372 cncrngOLD 21373 cnsrng 21389 pcoass 25034 clmvscom 25100 dvlipcn 26010 plydivlem4 26316 quotcan 26329 aaliou3lem3 26364 ef2kpi 26498 sinperlem 26500 sinmpi 26507 cosmpi 26508 sinppi 26509 cosppi 26510 sineq0 26543 tanregt0 26558 logneg 26607 lognegb 26609 logimul 26633 tanarg 26638 logtayl 26679 cxpsqrtlem 26721 cxpcom 26758 cubic2 26868 quart1 26876 log2cnv 26964 basellem1 27101 basellem3 27103 basellem5 27105 basellem8 27108 mumul 27201 chtublem 27232 perfectlem1 27250 perfectlem2 27251 perfect 27252 dchrabl 27275 bposlem6 27310 bposlem9 27313 lgsdir2lem4 27349 lgsdir2 27351 lgsquadlem2 27402 lgsquad2 27407 rpvmasum2 27533 mulog2sumlem1 27555 pntibndlem2 27612 pntibndlem3 27613 pntlemf 27626 nvscom 30554 ipasslem11 30765 ipblnfi 30780 hvmulcom 30968 h1de2bi 31479 homul12 31730 riesz3i 31987 riesz1 31990 kbass4 32044 sin2h 37259 heiborlem6 37465 rmym1 42530 expgrowthi 43944 expgrowth 43946 stoweidlem10 45568 perfectALTVlem1 47230 perfectALTVlem2 47231 perfectALTV 47232 tgoldbachlt 47325 2zrngnmlid2 47571 |
Copyright terms: Public domain | W3C validator |