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 10793, for naming consistency with mulcomi 10841. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 10793 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 (class class class)co 7213 ℂcc 10727 · cmul 10734 |
This theorem was proved from axioms: ax-mulcom 10793 |
This theorem is referenced by: adddir 10824 mulid2 10832 mulcomi 10841 mulcomd 10854 mul12 10997 mul32 10998 mul31 10999 mul4r 11001 mul01 11011 muladd 11264 subdir 11266 mulneg2 11269 recextlem1 11462 mulcan2g 11486 divmul3 11495 div23 11509 div13 11511 div12 11512 divmulasscom 11514 divcan4 11517 divmul13 11535 divmul24 11536 divcan7 11541 div2neg 11555 prodgt02 11680 ltmul2 11683 lemul2 11685 lemul2a 11687 ltmulgt12 11693 lemulge12 11695 ltmuldiv2 11706 ltdivmul2 11709 lt2mul2div 11710 ledivmul2 11711 lemuldiv2 11713 supmul 11804 times2 11967 modcyc 13479 modcyc2 13480 modmulmodr 13510 subsq 13778 cjmulrcl 14707 imval2 14714 abscj 14843 sqabsadd 14846 sqabssub 14847 sqreulem 14923 iseraltlem2 15246 iseraltlem3 15247 climcndslem2 15414 prodfmul 15454 prodmolem3 15495 bpoly3 15620 efcllem 15639 efexp 15662 sinmul 15733 demoivreALT 15762 dvdsmul1 15839 odd2np1lem 15901 odd2np1 15902 opeo 15926 omeo 15927 modgcd 16092 bezoutlem1 16099 dvdsgcd 16104 gcdmultipleOLD 16112 coprmdvds 16210 coprmdvds2 16211 qredeq 16214 eulerthlem2 16335 modprm0 16358 modprmn0modprm0 16360 coprimeprodsq2 16362 prmreclem6 16474 odmod 18938 cncrng 20384 cnsrng 20397 pcoass 23921 clmvscom 23987 dvlipcn 24891 plydivlem4 25189 quotcan 25202 aaliou3lem3 25237 ef2kpi 25368 sinperlem 25370 sinmpi 25377 cosmpi 25378 sinppi 25379 cosppi 25380 sineq0 25413 tanregt0 25428 logneg 25476 lognegb 25478 logimul 25502 tanarg 25507 logtayl 25548 cxpsqrtlem 25590 cxpcom 25625 cubic2 25731 quart1 25739 log2cnv 25827 basellem1 25963 basellem3 25965 basellem5 25967 basellem8 25970 mumul 26063 chtublem 26092 perfectlem1 26110 perfectlem2 26111 perfect 26112 dchrabl 26135 bposlem6 26170 bposlem9 26173 lgsdir2lem4 26209 lgsdir2 26211 lgsquadlem2 26262 lgsquad2 26267 rpvmasum2 26393 mulog2sumlem1 26415 pntibndlem2 26472 pntibndlem3 26473 pntlemf 26486 nvscom 28710 ipasslem11 28921 ipblnfi 28936 hvmulcom 29124 h1de2bi 29635 homul12 29886 riesz3i 30143 riesz1 30146 kbass4 30200 sin2h 35504 heiborlem6 35711 rmym1 40460 expgrowthi 41624 expgrowth 41626 stoweidlem10 43226 perfectALTVlem1 44846 perfectALTVlem2 44847 perfectALTV 44848 tgoldbachlt 44941 2zrngnmlid2 45182 |
Copyright terms: Public domain | W3C validator |