![]() |
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 | ⊢ (φ → A ∈ ℂ) |
addcld.2 | ⊢ (φ → B ∈ ℂ) |
Ref | Expression |
---|---|
addcld | ⊢ (φ → (A + B) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (φ → A ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (φ → B ∈ ℂ) | |
3 | addcl 6804 | . 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 391 | 1 ⊢ (φ → (A + B) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1390 (class class class)co 5455 ℂcc 6709 + caddc 6714 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-addcl 6779 |
This theorem is referenced by: negeu 6999 addsubass 7018 subsub2 7035 subsub4 7040 pnpcan 7046 pnncan 7048 addsub4 7050 apreim 7387 addext 7394 divdirap 7456 recp1lt1 7646 cju 7694 cnref1o 8357 expaddzap 8953 binom2 9015 binom3 9019 reval 9077 imval 9078 crre 9085 remullem 9099 imval2 9122 cjreim2 9132 cnrecnv 9138 |
Copyright terms: Public domain | W3C validator |