![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcl | GIF version |
Description: Alias for ax-addcl 7123, for naming consistency with addcli 7174. Use this theorem instead of ax-addcl 7123 or axaddcl 7083. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7123 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1434 (class class class)co 5537 ℂcc 7030 + caddc 7035 |
This theorem was proved from axioms: ax-addcl 7123 |
This theorem is referenced by: adddir 7161 0cn 7162 addcli 7174 addcld 7189 muladd11 7297 peano2cn 7299 muladd11r 7320 add4 7325 cnegexlem3 7341 cnegex 7342 0cnALT 7354 negeu 7355 pncan 7370 2addsub 7378 addsubeq4 7379 nppcan2 7395 ppncan 7406 muladd 7544 mulsub 7561 recexap 7799 muleqadd 7814 conjmulap 7873 halfaddsubcl 8320 halfaddsub 8321 iserf 9538 iseradd 9548 isersub 9549 iser0 9557 serige0 9559 serile 9560 binom2 9671 binom3 9676 bernneq 9679 shftlem 9831 shftval2 9841 shftval5 9844 2shfti 9846 crre 9871 crim 9872 cjadd 9898 addcj 9905 sqabsadd 10068 absreimsq 10080 absreim 10081 abstri 10117 addcn2 10276 climadd 10291 clim2iser 10302 clim2iser2 10303 iisermulc2 10305 iserile 10307 climserile 10310 serif0 10316 isumrblem 10326 fisumcvg 10327 opoe 10428 |
Copyright terms: Public domain | W3C validator |