![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcl | GIF version |
Description: Alias for ax-addcl 7906, for naming consistency with addcli 7960. Use this theorem instead of ax-addcl 7906 or axaddcl 7862. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7906 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 (class class class)co 5874 ℂcc 7808 + caddc 7813 |
This theorem was proved from axioms: ax-addcl 7906 |
This theorem is referenced by: adddir 7947 0cn 7948 addcli 7960 addcld 7975 muladd11 8088 peano2cn 8090 muladd11r 8111 add4 8116 cnegexlem3 8132 cnegex 8133 0cnALT 8145 negeu 8146 pncan 8161 2addsub 8169 addsubeq4 8170 nppcan2 8186 ppncan 8197 muladd 8339 mulsub 8356 recexap 8608 muleqadd 8623 conjmulap 8684 halfaddsubcl 9150 halfaddsub 9151 serf 10471 ser3add 10502 ser3sub 10503 ser0 10511 binom2 10628 binom3 10634 bernneq 10637 shftlem 10820 shftval2 10830 shftval5 10833 2shfti 10835 crre 10861 crim 10862 cjadd 10888 addcj 10895 sqabsadd 11059 absreimsq 11071 absreim 11072 abstri 11108 addcn2 11313 climadd 11329 clim2ser 11340 clim2ser2 11341 isermulc2 11343 serf0 11355 sumrbdclem 11380 fsum3cvg 11381 summodclem3 11383 summodclem2a 11384 zsumdc 11387 fsum3 11390 fsum3cvg2 11397 fsum3ser 11400 fsumcl2lem 11401 fsumcl 11403 sumsnf 11412 fsummulc2 11451 binom 11487 isumshft 11493 isumsplit 11494 geolim2 11515 cvgratnnlemseq 11529 cvgratz 11535 ef0lem 11663 efcj 11676 ef4p 11697 efgt1p 11699 tanval3ap 11717 efi4p 11720 sinadd 11739 cosadd 11740 tanaddap 11742 addsin 11745 demoivreALT 11776 opoe 11894 pythagtriplem4 12262 pythagtriplem12 12269 gzaddcl 12369 cncrng 13354 addccncf 13979 dvaddxxbr 14058 dvaddxx 14060 dviaddf 14062 dveflem 14080 sinperlem 14122 ptolemy 14138 tangtx 14152 sinkpi 14161 binom4 14290 2sqlem2 14344 |
Copyright terms: Public domain | W3C validator |