Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcl | GIF version |
Description: Alias for ax-addcl 7072, for naming consistency with addcli 7123. Use this theorem instead of ax-addcl 7072 or axaddcl 7032. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7072 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1433 (class class class)co 5532 ℂcc 6979 + caddc 6984 |
This theorem was proved from axioms: ax-addcl 7072 |
This theorem is referenced by: adddir 7110 0cn 7111 addcli 7123 addcld 7138 muladd11 7241 peano2cn 7243 muladd11r 7264 add4 7269 cnegexlem3 7285 cnegex 7286 0cnALT 7298 negeu 7299 pncan 7314 2addsub 7322 addsubeq4 7323 nppcan2 7339 ppncan 7350 muladd 7488 mulsub 7505 recexap 7743 muleqadd 7758 conjmulap 7817 halfaddsubcl 8264 halfaddsub 8265 iserf 9453 iseradd 9463 isersub 9464 iser0 9471 iser0f 9472 serige0 9473 serile 9474 binom2 9585 binom3 9590 bernneq 9593 shftlem 9704 shftval2 9714 shftval5 9717 2shfti 9719 crre 9744 crim 9745 cjadd 9771 addcj 9778 sqabsadd 9941 absreimsq 9953 absreim 9954 abstri 9990 addcn2 10149 climadd 10164 clim2iser 10175 clim2iser2 10176 iisermulc2 10178 iserile 10180 climserile 10183 serif0 10189 opoe 10295 |
Copyright terms: Public domain | W3C validator |