![]() |
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 7530 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 404 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 (class class class)co 5668 ℂcc 7411 + caddc 7416 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 ax-addcl 7504 |
This theorem is referenced by: muladd11r 7701 negeu 7736 addsubass 7755 subsub2 7773 subsub4 7778 pnpcan 7784 pnncan 7786 addsub4 7788 pnpncand 7916 apreim 8143 addext 8150 divdirap 8227 recp1lt1 8423 cju 8484 cnref1o 9196 modsumfzodifsn 9866 ser3add 9998 expaddzap 10062 binom2 10128 binom3 10134 sqoddm1div8 10169 nn0opthlem1d 10191 reval 10346 imval 10347 crre 10354 remullem 10368 imval2 10391 cjreim2 10401 cnrecnv 10407 resqrexlemcalc1 10510 maxabslemab 10702 maxltsup 10714 max0addsup 10715 addcn2 10762 fsumadd 10863 isumadd 10888 binomlem 10940 efaddlem 11027 ef4p 11047 cosval 11057 cosf 11059 tanval2ap 11067 tanval3ap 11068 resin4p 11072 recos4p 11073 efival 11086 sinadd 11090 cosadd 11091 tanaddap 11093 oddennn 11546 qdencn 12218 |
Copyright terms: Public domain | W3C validator |