![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcom | Unicode version |
Description: Alias for ax-mulcom 7745, for naming consistency with mulcomi 7796. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7745 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcom 7745 |
This theorem is referenced by: adddir 7781 mulid2 7788 mulcomi 7796 mulcomd 7811 mul12 7915 mul32 7916 mul31 7917 muladd 8170 subdir 8172 mul01 8175 mulneg2 8182 recextlem1 8436 divmulap3 8461 div23ap 8475 div13ap 8477 div12ap 8478 divmulasscomap 8480 divcanap4 8483 divmul13ap 8499 divmul24ap 8500 divcanap7 8505 div2negap 8519 prodgt02 8635 prodge02 8637 ltmul2 8638 lemul2 8639 lemul2a 8641 ltmulgt12 8647 lemulge12 8649 ltmuldiv2 8657 ltdivmul2 8660 ledivmul2 8662 lemuldiv2 8664 times2 8873 modqcyc2 10164 subsq 10430 cjmulrcl 10691 imval2 10698 abscj 10856 sqabsadd 10859 sqabssub 10860 prod3fmul 11342 prodmodclem3 11376 efcllemp 11401 efexp 11425 sinmul 11487 demoivreALT 11516 dvdsmul1 11551 odd2np1lem 11605 odd2np1 11606 opeo 11630 omeo 11631 modgcd 11715 dvdsgcd 11736 gcdmultiple 11744 coprmdvds 11809 coprmdvds2 11810 qredeq 11813 ef2kpi 12935 sinperlem 12937 sinmpi 12944 cosmpi 12945 sinppi 12946 cosppi 12947 cxpcom 13065 |
Copyright terms: Public domain | W3C validator |