![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcl | Unicode version |
Description: Alias for ax-mulcl 7506, for naming consistency with mulcli 7556. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcl 7506 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mulcl 7506 |
This theorem is referenced by: 0cn 7543 mulid1 7548 mulcli 7556 mulcld 7571 mul31 7676 mul4 7677 muladd11r 7701 cnegexlem2 7721 cnegex 7723 muladd 7925 subdi 7926 mul02 7928 submul2 7940 mulsub 7942 recextlem1 8183 recexap 8185 muleqadd 8200 divassap 8220 divmulassap 8225 divmuldivap 8242 divmuleqap 8247 divadddivap 8257 conjmulap 8259 cju 8484 zneo 8910 exp3vallem 10019 exp3val 10020 exp1 10024 expp1 10025 expcl 10036 expclzaplem 10042 mulexp 10057 sqcl 10079 subsq 10124 subsq2 10125 binom2sub 10130 mulbinom2 10133 binom3 10134 zesq 10135 bernneq 10137 bernneq2 10138 facnn 10198 fac0 10199 fac1 10200 facp1 10201 ibcval5 10234 bcn2 10235 reim 10349 imcl 10351 crre 10354 crim 10355 remim 10357 mulreap 10361 cjreb 10363 recj 10364 reneg 10365 readd 10366 remullem 10368 remul2 10370 imcj 10372 imneg 10373 imadd 10374 immul2 10377 cjadd 10381 ipcnval 10383 cjmulrcl 10384 cjneg 10387 imval2 10391 cjreim 10400 rennim 10498 sqabsadd 10551 sqabssub 10552 absreimsq 10563 absreim 10564 absmul 10565 mulcn2 10764 climmul 10778 iisermulc2 10791 fsummulc2 10905 efexp 11035 sinf 11058 cosf 11059 tanval2ap 11067 tanval3ap 11068 resinval 11069 recosval 11070 efi4p 11071 resin4p 11072 recos4p 11073 resincl 11074 recoscl 11075 sinneg 11080 cosneg 11081 efival 11086 efmival 11087 efeul 11088 sinadd 11090 cosadd 11091 sinsub 11094 cossub 11095 subsin 11097 sinmul 11098 cosmul 11099 addcos 11100 subcos 11101 cos2tsin 11105 ef01bndlem 11110 sin01bnd 11111 cos01bnd 11112 absef 11122 absefib 11123 efieq1re 11124 demoivre 11125 demoivreALT 11126 odd2np1lem 11213 odd2np1 11214 opoe 11236 omoe 11237 opeo 11238 omeo 11239 modgcd 11323 qredeq 11419 mulc1cncf 11949 |
Copyright terms: Public domain | W3C validator |