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 8381 muleqadd 8396 conjmulap 8456 halfaddsubcl 8911 halfaddsub 8912 serf 10202 ser3add 10233 ser3sub 10234 ser0 10242 binom2 10358 binom3 10364 bernneq 10367 shftlem 10543 shftval2 10553 shftval5 10556 2shfti 10558 crre 10584 crim 10585 cjadd 10611 addcj 10618 sqabsadd 10782 absreimsq 10794 absreim 10795 abstri 10831 addcn2 11034 climadd 11050 clim2ser 11061 clim2ser2 11062 isermulc2 11064 serf0 11076 sumrbdclem 11100 fsum3cvg 11101 summodclem3 11104 summodclem2a 11105 zsumdc 11108 fsum3 11111 fsum3cvg2 11118 fsum3ser 11121 fsumcl2lem 11122 fsumcl 11124 sumsnf 11133 fsummulc2 11172 binom 11208 isumshft 11214 isumsplit 11215 geolim2 11236 cvgratnnlemseq 11250 cvgratz 11256 ef0lem 11280 efcj 11293 ef4p 11314 efgt1p 11316 tanval3ap 11335 efi4p 11338 sinadd 11357 cosadd 11358 tanaddap 11360 addsin 11363 demoivreALT 11394 opoe 11504 addccncf 12666 dvaddxxbr 12745 dvaddxx 12747 dviaddf 12749 dveflem 12766 sinperlem 12800 ptolemy 12816 |
Copyright terms: Public domain | W3C validator |