![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcom | Unicode version |
Description: Alias for ax-mulcom 7943, for naming consistency with mulcomi 7994. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7943 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcom 7943 |
This theorem is referenced by: adddir 7979 mullid 7986 mulcomi 7994 mulcomd 8010 mul12 8117 mul32 8118 mul31 8119 muladd 8372 subdir 8374 mul01 8377 mulneg2 8384 recextlem1 8639 divmulap3 8665 div23ap 8679 div13ap 8681 div12ap 8682 divmulasscomap 8684 divcanap4 8687 divmul13ap 8703 divmul24ap 8704 divcanap7 8709 div2negap 8723 prodgt02 8841 prodge02 8843 ltmul2 8844 lemul2 8845 lemul2a 8847 ltmulgt12 8853 lemulge12 8855 ltmuldiv2 8863 ltdivmul2 8866 ledivmul2 8868 lemuldiv2 8870 times2 9079 modqcyc2 10393 subsq 10661 cjmulrcl 10931 imval2 10938 abscj 11096 sqabsadd 11099 sqabssub 11100 prod3fmul 11584 prodmodclem3 11618 efcllemp 11701 efexp 11725 sinmul 11787 demoivreALT 11816 dvdsmul1 11855 odd2np1lem 11912 odd2np1 11913 opeo 11937 omeo 11938 modgcd 12027 dvdsgcd 12048 gcdmultiple 12056 coprmdvds 12127 coprmdvds2 12128 qredeq 12131 modprm0 12289 modprmn0modprm0 12291 coprimeprodsq2 12293 cncrng 13889 ef2kpi 14704 sinperlem 14706 sinmpi 14713 cosmpi 14714 sinppi 14715 cosppi 14716 cxpcom 14834 lgsdir2lem4 14910 lgsdir2 14912 |
Copyright terms: Public domain | W3C validator |