Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcl | GIF version |
Description: Alias for ax-addcl 7716, for naming consistency with addcli 7770. Use this theorem instead of ax-addcl 7716 or axaddcl 7672. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7716 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1480 (class class class)co 5774 ℂcc 7618 + caddc 7623 |
This theorem was proved from axioms: ax-addcl 7716 |
This theorem is referenced by: adddir 7757 0cn 7758 addcli 7770 addcld 7785 muladd11 7895 peano2cn 7897 muladd11r 7918 add4 7923 cnegexlem3 7939 cnegex 7940 0cnALT 7952 negeu 7953 pncan 7968 2addsub 7976 addsubeq4 7977 nppcan2 7993 ppncan 8004 muladd 8146 mulsub 8163 recexap 8414 muleqadd 8429 conjmulap 8489 halfaddsubcl 8953 halfaddsub 8954 serf 10247 ser3add 10278 ser3sub 10279 ser0 10287 binom2 10403 binom3 10409 bernneq 10412 shftlem 10588 shftval2 10598 shftval5 10601 2shfti 10603 crre 10629 crim 10630 cjadd 10656 addcj 10663 sqabsadd 10827 absreimsq 10839 absreim 10840 abstri 10876 addcn2 11079 climadd 11095 clim2ser 11106 clim2ser2 11107 isermulc2 11109 serf0 11121 sumrbdclem 11146 fsum3cvg 11147 summodclem3 11149 summodclem2a 11150 zsumdc 11153 fsum3 11156 fsum3cvg2 11163 fsum3ser 11166 fsumcl2lem 11167 fsumcl 11169 sumsnf 11178 fsummulc2 11217 binom 11253 isumshft 11259 isumsplit 11260 geolim2 11281 cvgratnnlemseq 11295 cvgratz 11301 ef0lem 11366 efcj 11379 ef4p 11400 efgt1p 11402 tanval3ap 11421 efi4p 11424 sinadd 11443 cosadd 11444 tanaddap 11446 addsin 11449 demoivreALT 11480 opoe 11592 addccncf 12755 dvaddxxbr 12834 dvaddxx 12836 dviaddf 12838 dveflem 12855 sinperlem 12889 ptolemy 12905 tangtx 12919 sinkpi 12928 |
Copyright terms: Public domain | W3C validator |