![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcl | Unicode version |
Description: Alias for ax-addcl 7439, for naming consistency with addcli 7490. Use this theorem instead of ax-addcl 7439 or axaddcl 7399. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7439 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-addcl 7439 |
This theorem is referenced by: adddir 7477 0cn 7478 addcli 7490 addcld 7505 muladd11 7613 peano2cn 7615 muladd11r 7636 add4 7641 cnegexlem3 7657 cnegex 7658 0cnALT 7670 negeu 7671 pncan 7686 2addsub 7694 addsubeq4 7695 nppcan2 7711 ppncan 7722 muladd 7860 mulsub 7877 recexap 8120 muleqadd 8135 conjmulap 8194 halfaddsubcl 8647 halfaddsub 8648 serf 9896 iseqseq3 9898 iserf 9899 iseradd 9930 isersub 9932 iser0 9943 ser0 9945 binom2 10061 binom3 10067 bernneq 10070 shftlem 10246 shftval2 10256 shftval5 10259 2shfti 10261 crre 10287 crim 10288 cjadd 10314 addcj 10321 sqabsadd 10484 absreimsq 10496 absreim 10497 abstri 10533 addcn2 10695 climadd 10710 clim2ser 10721 clim2ser2 10722 iisermulc2 10724 serf0 10737 isumrblem 10761 fisumcvg 10762 fsum3cvg 10763 isummolem3 10766 isummolem2a 10767 zisum 10770 fisum 10774 fisumcvg2 10782 fsum3cvg2 10783 fisumser 10786 fsumcl2lem 10788 fsumcl 10790 sumsnf 10799 fsummulc2 10838 binom 10874 isumshft 10880 isumsplit 10881 geolim2 10902 cvgratnnlemseq 10916 cvgratz 10922 ef0lem 10946 efcj 10959 ef4p 10980 efgt1p 10982 tanval3ap 11001 efi4p 11004 sinadd 11023 cosadd 11024 tanaddap 11026 addsin 11029 demoivreALT 11059 opoe 11169 |
Copyright terms: Public domain | W3C validator |