![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcom | Unicode version |
Description: Alias for ax-mulcom 7596, for naming consistency with mulcomi 7644. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7596 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcom 7596 |
This theorem is referenced by: adddir 7629 mulid2 7636 mulcomi 7644 mulcomd 7659 mul12 7762 mul32 7763 mul31 7764 muladd 8013 subdir 8015 mul01 8018 mulneg2 8025 recextlem1 8273 divmulap3 8298 div23ap 8312 div13ap 8314 div12ap 8315 divmulasscomap 8317 divcanap4 8320 divmul13ap 8336 divmul24ap 8337 divcanap7 8342 div2negap 8356 prodgt02 8469 prodge02 8471 ltmul2 8472 lemul2 8473 lemul2a 8475 ltmulgt12 8481 lemulge12 8483 ltmuldiv2 8491 ltdivmul2 8494 ledivmul2 8496 lemuldiv2 8498 times2 8701 modqcyc2 9974 subsq 10240 cjmulrcl 10500 imval2 10507 abscj 10664 sqabsadd 10667 sqabssub 10668 efcllemp 11162 efexp 11186 sinmul 11249 demoivreALT 11277 dvdsmul1 11310 odd2np1lem 11364 odd2np1 11365 opeo 11389 omeo 11390 modgcd 11474 dvdsgcd 11493 gcdmultiple 11501 coprmdvds 11566 coprmdvds2 11567 qredeq 11570 |
Copyright terms: Public domain | W3C validator |