Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mulcl | Unicode version |
Description: Alias for ax-mulcl 7686, for naming consistency with mulcli 7739. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
mulcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulcl 7686 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 (class class class)co 5742 cc 7586 cmul 7593 |
This theorem was proved from axioms: ax-mulcl 7686 |
This theorem is referenced by: 0cn 7726 mulid1 7731 mulcli 7739 mulcld 7754 mul31 7861 mul4 7862 muladd11r 7886 cnegexlem2 7906 cnegex 7908 muladd 8114 subdi 8115 mul02 8117 submul2 8129 mulsub 8131 recextlem1 8380 recexap 8382 muleqadd 8397 divassap 8418 divmulassap 8423 divmuldivap 8440 divmuleqap 8445 divadddivap 8455 conjmulap 8457 cju 8687 zneo 9120 exp3vallem 10262 exp3val 10263 exp1 10267 expp1 10268 expcl 10279 expclzaplem 10285 mulexp 10300 sqcl 10322 subsq 10367 subsq2 10368 binom2sub 10373 mulbinom2 10376 binom3 10377 zesq 10378 bernneq 10380 bernneq2 10381 facnn 10441 fac0 10442 fac1 10443 facp1 10444 bcval5 10477 bcn2 10478 reim 10592 imcl 10594 crre 10597 crim 10598 remim 10600 mulreap 10604 cjreb 10606 recj 10607 reneg 10608 readd 10609 remullem 10611 remul2 10613 imcj 10615 imneg 10616 imadd 10617 immul2 10620 cjadd 10624 ipcnval 10626 cjmulrcl 10627 cjneg 10630 imval2 10634 cjreim 10643 rennim 10742 sqabsadd 10795 sqabssub 10796 absreimsq 10807 absreim 10808 absmul 10809 mul0inf 10980 mulcn2 11049 climmul 11064 isermulc2 11077 fsummulc2 11185 efexp 11315 sinf 11338 cosf 11339 tanval2ap 11347 tanval3ap 11348 resinval 11349 recosval 11350 efi4p 11351 resin4p 11352 recos4p 11353 resincl 11354 recoscl 11355 sinneg 11360 cosneg 11361 efival 11366 efmival 11367 efeul 11368 sinadd 11370 cosadd 11371 sinsub 11374 cossub 11375 subsin 11377 sinmul 11378 cosmul 11379 addcos 11380 subcos 11381 cos2tsin 11385 ef01bndlem 11390 sin01bnd 11391 cos01bnd 11392 absef 11403 absefib 11404 efieq1re 11405 demoivre 11406 demoivreALT 11407 odd2np1lem 11496 odd2np1 11497 opoe 11519 omoe 11520 opeo 11521 omeo 11522 modgcd 11606 qredeq 11704 mulc1cncf 12672 mulcncflem 12686 dvmulxxbr 12762 dvmulxx 12764 dvimulf 12766 efper 12815 sinperlem 12816 sin2kpi 12819 cos2kpi 12820 efimpi 12827 sincosq1eq 12847 abssinper 12854 sinkpi 12855 coskpi 12856 |
Copyright terms: Public domain | W3C validator |