Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > readdcl | GIF version |
Description: Alias for ax-addrcl 6981, for naming consistency with readdcli 7040. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
readdcl | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addrcl 6981 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1393 (class class class)co 5512 ℝcr 6888 + caddc 6892 |
This theorem was proved from axioms: ax-addrcl 6981 |
This theorem is referenced by: 0re 7027 readdcli 7040 readdcld 7055 axltadd 7089 peano2re 7149 cnegexlem3 7188 cnegex 7189 resubcl 7275 ltleadd 7441 ltaddsublt 7562 recexap 7634 recreclt 7866 cju 7913 nnge1 7937 addltmul 8161 avglt1 8163 avglt2 8164 avgle1 8165 avgle2 8166 irradd 8580 rpaddcl 8606 iooshf 8821 ge0addcl 8850 icoshft 8858 icoshftf1o 8859 iccshftr 8862 difelfznle 8993 elfzodifsumelfzo 9057 subfzo0 9097 iserfre 9234 isermono 9237 serige0 9252 serile 9253 bernneq 9369 readd 9469 imadd 9477 elicc4abs 9690 caubnd2 9713 mulcn2 9833 iserile 9862 climserile 9865 |
Copyright terms: Public domain | W3C validator |