Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcom | GIF version |
Description: Alias for ax-mulcom 7875, for naming consistency with mulcomi 7926. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7875 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1348 ∈ wcel 2141 (class class class)co 5853 ℂcc 7772 · cmul 7779 |
This theorem was proved from axioms: ax-mulcom 7875 |
This theorem is referenced by: adddir 7911 mulid2 7918 mulcomi 7926 mulcomd 7941 mul12 8048 mul32 8049 mul31 8050 muladd 8303 subdir 8305 mul01 8308 mulneg2 8315 recextlem1 8569 divmulap3 8594 div23ap 8608 div13ap 8610 div12ap 8611 divmulasscomap 8613 divcanap4 8616 divmul13ap 8632 divmul24ap 8633 divcanap7 8638 div2negap 8652 prodgt02 8769 prodge02 8771 ltmul2 8772 lemul2 8773 lemul2a 8775 ltmulgt12 8781 lemulge12 8783 ltmuldiv2 8791 ltdivmul2 8794 ledivmul2 8796 lemuldiv2 8798 times2 9007 modqcyc2 10316 subsq 10582 cjmulrcl 10851 imval2 10858 abscj 11016 sqabsadd 11019 sqabssub 11020 prod3fmul 11504 prodmodclem3 11538 efcllemp 11621 efexp 11645 sinmul 11707 demoivreALT 11736 dvdsmul1 11775 odd2np1lem 11831 odd2np1 11832 opeo 11856 omeo 11857 modgcd 11946 dvdsgcd 11967 gcdmultiple 11975 coprmdvds 12046 coprmdvds2 12047 qredeq 12050 modprm0 12208 modprmn0modprm0 12210 coprimeprodsq2 12212 ef2kpi 13521 sinperlem 13523 sinmpi 13530 cosmpi 13531 sinppi 13532 cosppi 13533 cxpcom 13651 lgsdir2lem4 13726 lgsdir2 13728 |
Copyright terms: Public domain | W3C validator |