Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcl | Unicode version |
Description: Alias for ax-addcl 7684, for naming consistency with addcli 7738. Use this theorem instead of ax-addcl 7684 or axaddcl 7640. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7684 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wcel 1465 (class class class)co 5742 cc 7586 caddc 7591 |
This theorem was proved from axioms: ax-addcl 7684 |
This theorem is referenced by: adddir 7725 0cn 7726 addcli 7738 addcld 7753 muladd11 7863 peano2cn 7865 muladd11r 7886 add4 7891 cnegexlem3 7907 cnegex 7908 0cnALT 7920 negeu 7921 pncan 7936 2addsub 7944 addsubeq4 7945 nppcan2 7961 ppncan 7972 muladd 8114 mulsub 8131 recexap 8382 muleqadd 8397 conjmulap 8457 halfaddsubcl 8921 halfaddsub 8922 serf 10215 ser3add 10246 ser3sub 10247 ser0 10255 binom2 10371 binom3 10377 bernneq 10380 shftlem 10556 shftval2 10566 shftval5 10569 2shfti 10571 crre 10597 crim 10598 cjadd 10624 addcj 10631 sqabsadd 10795 absreimsq 10807 absreim 10808 abstri 10844 addcn2 11047 climadd 11063 clim2ser 11074 clim2ser2 11075 isermulc2 11077 serf0 11089 sumrbdclem 11113 fsum3cvg 11114 summodclem3 11117 summodclem2a 11118 zsumdc 11121 fsum3 11124 fsum3cvg2 11131 fsum3ser 11134 fsumcl2lem 11135 fsumcl 11137 sumsnf 11146 fsummulc2 11185 binom 11221 isumshft 11227 isumsplit 11228 geolim2 11249 cvgratnnlemseq 11263 cvgratz 11269 ef0lem 11293 efcj 11306 ef4p 11327 efgt1p 11329 tanval3ap 11348 efi4p 11351 sinadd 11370 cosadd 11371 tanaddap 11373 addsin 11376 demoivreALT 11407 opoe 11519 addccncf 12682 dvaddxxbr 12761 dvaddxx 12763 dviaddf 12765 dveflem 12782 sinperlem 12816 ptolemy 12832 tangtx 12846 sinkpi 12855 |
Copyright terms: Public domain | W3C validator |