![]() |
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 7961 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 (class class class)co 5892 ℂcc 7834 + caddc 7839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-addcl 7932 |
This theorem is referenced by: muladd11r 8138 negeu 8173 addsubass 8192 subsub2 8210 subsub4 8215 pnpcan 8221 pnncan 8223 addsub4 8225 pnpncand 8357 apreim 8585 addext 8592 aprcl 8628 aptap 8632 divdirap 8679 recp1lt1 8881 cju 8943 cnref1o 9675 modsumfzodifsn 10422 expaddzap 10590 binom2 10658 binom3 10664 sqoddm1div8 10700 mulsubdivbinom2ap 10718 nn0opthlem1d 10727 reval 10885 imval 10886 crre 10893 remullem 10907 imval2 10930 cjreim2 10940 cnrecnv 10946 resqrexlemcalc1 11050 maxabslemab 11242 maxltsup 11254 max0addsup 11255 minabs 11271 bdtrilem 11274 bdtri 11275 addcn2 11345 fsumadd 11441 isumadd 11466 binomlem 11518 efaddlem 11709 ef4p 11729 cosval 11738 cosf 11740 tanval2ap 11748 tanval3ap 11749 resin4p 11753 recos4p 11754 efival 11767 sinadd 11771 cosadd 11772 tanaddap 11774 pythagtriplem1 12292 pythagtriplem12 12302 pythagtriplem16 12306 pythagtriplem17 12307 pcbc 12378 mul4sqlem 12420 4sqlem14 12431 oddennn 12438 mulgdirlem 13086 addccncf 14523 limcimolemlt 14570 dvaddxxbr 14602 ptolemy 14682 rpcxpadd 14763 binom4 14834 qdencn 15213 iooref1o 15220 apdifflemr 15233 |
Copyright terms: Public domain | W3C validator |