![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcl | Unicode version |
Description: Alias for ax-mulcl 7940, for naming consistency with mulcli 7993. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcl 7940 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcl 7940 |
This theorem is referenced by: 0cn 7980 mulrid 7985 mulcli 7993 mulcld 8009 mul31 8119 mul4 8120 muladd11r 8144 cnegexlem2 8164 cnegex 8166 muladd 8372 subdi 8373 mul02 8375 submul2 8387 mulsub 8389 recextlem1 8639 recexap 8641 muleqadd 8656 divassap 8678 divmulassap 8683 divmuldivap 8700 divmuleqap 8705 divadddivap 8715 conjmulap 8717 cju 8949 zneo 9385 exp3vallem 10555 exp3val 10556 exp1 10560 expp1 10561 expcl 10572 expclzaplem 10578 mulexp 10593 sqcl 10615 subsq 10661 subsq2 10662 binom2sub 10668 mulbinom2 10671 binom3 10672 zesq 10673 bernneq 10675 bernneq2 10676 mulsubdivbinom2ap 10726 facnn 10742 fac0 10743 fac1 10744 facp1 10745 bcval5 10778 bcn2 10779 reim 10896 imcl 10898 crre 10901 crim 10902 remim 10904 mulreap 10908 cjreb 10910 recj 10911 reneg 10912 readd 10913 remullem 10915 remul2 10917 imcj 10919 imneg 10920 imadd 10921 immul2 10924 cjadd 10928 ipcnval 10930 cjmulrcl 10931 cjneg 10934 imval2 10938 cjreim 10947 rennim 11046 sqabsadd 11099 sqabssub 11100 absreimsq 11111 absreim 11112 absmul 11113 mul0inf 11284 mulcn2 11355 climmul 11370 isermulc2 11383 fsummulc2 11491 prodf 11581 clim2prod 11582 clim2divap 11583 prod3fmul 11584 prodf1 11585 prodfap0 11588 prodfrecap 11589 prodrbdclem 11614 fproddccvg 11615 prodmodclem3 11618 prodmodclem2a 11619 zproddc 11622 fprodseq 11626 fprodntrivap 11627 prodsnf 11635 fprodcl 11650 fprodclf 11678 efexp 11725 sinf 11747 cosf 11748 tanval2ap 11756 tanval3ap 11757 resinval 11758 recosval 11759 efi4p 11760 resin4p 11761 recos4p 11762 resincl 11763 recoscl 11764 sinneg 11769 cosneg 11770 efival 11775 efmival 11776 efeul 11777 sinadd 11779 cosadd 11780 sinsub 11783 cossub 11784 subsin 11786 sinmul 11787 cosmul 11788 addcos 11789 subcos 11790 cos2tsin 11794 ef01bndlem 11799 sin01bnd 11800 cos01bnd 11801 absef 11812 absefib 11813 efieq1re 11814 demoivre 11815 demoivreALT 11816 odd2np1lem 11912 odd2np1 11913 opoe 11935 omoe 11936 opeo 11937 omeo 11938 modgcd 12027 qredeq 12131 modprm0 12289 pythagtriplem1 12300 pythagtriplem12 12310 pythagtriplem14 12312 gzmulcl 12413 4sqlem11 12436 4sqlem17 12442 cncrng 13889 cnfldmulg 13896 mulc1cncf 14553 mulcncflem 14567 dvmulxxbr 14643 dvmulxx 14645 dvimulf 14647 efper 14705 sinperlem 14706 sin2kpi 14709 cos2kpi 14710 efimpi 14717 sincosq1eq 14737 abssinper 14744 sinkpi 14745 coskpi 14746 binom4 14874 lgsdilem2 14915 lgsne0 14917 2sqlem2 14940 |
Copyright terms: Public domain | W3C validator |