![]() |
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 10450, for naming consistency with mulcomi 10498. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 10450 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 (class class class)co 7019 ℂcc 10384 · cmul 10391 |
This theorem was proved from axioms: ax-mulcom 10450 |
This theorem is referenced by: adddir 10481 mulid2 10489 mulcomi 10498 mulcomd 10511 mul12 10654 mul32 10655 mul31 10656 mul4r 10658 mul01 10668 muladd 10922 subdir 10924 mulneg2 10927 recextlem1 11120 mulcan2g 11144 divmul3 11153 div23 11167 div13 11169 div12 11170 divmulasscom 11172 divcan4 11175 divmul13 11193 divmul24 11194 divcan7 11199 div2neg 11213 prodgt02 11338 ltmul2 11341 lemul2 11343 lemul2a 11345 ltmulgt12 11351 lemulge12 11353 ltmuldiv2 11364 ltdivmul2 11367 lt2mul2div 11368 ledivmul2 11369 lemuldiv2 11371 supmul 11463 times2 11624 modcyc 13124 modcyc2 13125 modmulmodr 13155 subsq 13422 cjmulrcl 14337 imval2 14344 abscj 14473 sqabsadd 14476 sqabssub 14477 sqreulem 14553 iseraltlem2 14873 iseraltlem3 14874 climcndslem2 15038 prodfmul 15079 prodmolem3 15120 bpoly3 15245 efcllem 15264 efexp 15287 sinmul 15358 demoivreALT 15387 dvdsmul1 15464 odd2np1lem 15522 odd2np1 15523 opeo 15547 omeo 15548 modgcd 15713 bezoutlem1 15716 dvdsgcd 15721 gcdmultiple 15729 coprmdvds 15826 coprmdvds2 15827 qredeq 15830 eulerthlem2 15948 modprm0 15971 modprmn0modprm0 15973 coprimeprodsq2 15975 prmreclem6 16086 odmod 18405 cncrng 20248 cnsrng 20261 pcoass 23311 clmvscom 23377 dvlipcn 24274 plydivlem4 24568 quotcan 24581 aaliou3lem3 24616 ef2kpi 24747 sinperlem 24749 sinmpi 24756 cosmpi 24757 sinppi 24758 cosppi 24759 sineq0 24792 tanregt0 24804 logneg 24852 lognegb 24854 logimul 24878 tanarg 24883 logtayl 24924 cxpsqrtlem 24966 cxpcom 25001 cubic2 25107 quart1 25115 log2cnv 25204 basellem1 25340 basellem3 25342 basellem5 25344 basellem8 25347 mumul 25440 chtublem 25469 perfectlem1 25487 perfectlem2 25488 perfect 25489 dchrabl 25512 bposlem6 25547 bposlem9 25550 lgsdir2lem4 25586 lgsdir2 25588 lgsquadlem2 25639 lgsquad2 25644 rpvmasum2 25770 mulog2sumlem1 25792 pntibndlem2 25849 pntibndlem3 25850 pntlemf 25863 nvscom 28089 ipasslem11 28300 ipblnfi 28315 hvmulcom 28503 h1de2bi 29014 homul12 29265 riesz3i 29522 riesz1 29525 kbass4 29579 sin2h 34426 heiborlem6 34639 rmym1 39030 expgrowthi 40216 expgrowth 40218 stoweidlem10 41851 perfectALTVlem1 43382 perfectALTVlem2 43383 perfectALTV 43384 tgoldbachlt 43477 2zrngnmlid2 43714 |
Copyright terms: Public domain | W3C validator |