Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcld | GIF version |
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
addcld | ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addcl 7006 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 391 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 + caddc 6892 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-addcl 6980 |
This theorem is referenced by: negeu 7202 addsubass 7221 subsub2 7239 subsub4 7244 pnpcan 7250 pnncan 7252 addsub4 7254 apreim 7594 addext 7601 divdirap 7674 recp1lt1 7865 cju 7913 cnref1o 8582 expaddzap 9299 binom2 9362 binom3 9366 reval 9449 imval 9450 crre 9457 remullem 9471 imval2 9494 cjreim2 9504 cnrecnv 9510 resqrexlemcalc1 9612 addcn2 9831 qdencn 10124 |
Copyright terms: Public domain | W3C validator |