![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcom | Unicode version |
Description: Alias for ax-mulcom 7911, for naming consistency with mulcomi 7962. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcom 7911 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcom 7911 |
This theorem is referenced by: adddir 7947 mullid 7954 mulcomi 7962 mulcomd 7978 mul12 8085 mul32 8086 mul31 8087 muladd 8340 subdir 8342 mul01 8345 mulneg2 8352 recextlem1 8607 divmulap3 8633 div23ap 8647 div13ap 8649 div12ap 8650 divmulasscomap 8652 divcanap4 8655 divmul13ap 8671 divmul24ap 8672 divcanap7 8677 div2negap 8691 prodgt02 8809 prodge02 8811 ltmul2 8812 lemul2 8813 lemul2a 8815 ltmulgt12 8821 lemulge12 8823 ltmuldiv2 8831 ltdivmul2 8834 ledivmul2 8836 lemuldiv2 8838 times2 9047 modqcyc2 10359 subsq 10626 cjmulrcl 10895 imval2 10902 abscj 11060 sqabsadd 11063 sqabssub 11064 prod3fmul 11548 prodmodclem3 11582 efcllemp 11665 efexp 11689 sinmul 11751 demoivreALT 11780 dvdsmul1 11819 odd2np1lem 11876 odd2np1 11877 opeo 11901 omeo 11902 modgcd 11991 dvdsgcd 12012 gcdmultiple 12020 coprmdvds 12091 coprmdvds2 12092 qredeq 12095 modprm0 12253 modprmn0modprm0 12255 coprimeprodsq2 12257 cncrng 13433 ef2kpi 14197 sinperlem 14199 sinmpi 14206 cosmpi 14207 sinppi 14208 cosppi 14209 cxpcom 14327 lgsdir2lem4 14402 lgsdir2 14404 |
Copyright terms: Public domain | W3C validator |