| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > addcld | Unicode 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 8157 |
. 2
| |
| 4 | 1, 2, 3 | syl2anc 411 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-addcl 8128 |
| This theorem is referenced by: muladd11r 8335 negeu 8370 addsubass 8389 subsub2 8407 subsub4 8412 pnpcan 8418 pnncan 8420 addsub4 8422 pnpncand 8554 apreim 8783 addext 8790 aprcl 8826 aptap 8830 divdirap 8877 recp1lt1 9079 cju 9141 cnref1o 9885 modsumfzodifsn 10659 expaddzap 10846 binom2 10914 binom3 10920 sqoddm1div8 10956 mulsubdivbinom2ap 10974 nn0opthlem1d 10983 reval 11411 imval 11412 crre 11419 remullem 11433 imval2 11456 cjreim2 11466 cnrecnv 11472 resqrexlemcalc1 11576 maxabslemab 11768 maxltsup 11780 max0addsup 11781 minabs 11798 bdtrilem 11801 bdtri 11802 addcn2 11872 fsumadd 11969 isumadd 11994 binomlem 12046 efaddlem 12237 ef4p 12257 cosval 12266 cosf 12268 tanval2ap 12276 tanval3ap 12277 resin4p 12281 recos4p 12282 efival 12295 sinadd 12299 cosadd 12300 tanaddap 12302 pythagtriplem1 12840 pythagtriplem12 12850 pythagtriplem16 12854 pythagtriplem17 12855 pcbc 12926 mul4sqlem 12968 4sqlem14 12979 oddennn 13015 mulgdirlem 13742 gsumfzconst 13930 gsumfzfsumlemm 14604 addccncf 15327 limcimolemlt 15391 dvaddxxbr 15428 plyaddlem1 15474 ptolemy 15551 rpcxpadd 15632 binom4 15706 lgsquad2lem1 15813 2lgslem3d1 15832 qdencn 16648 iooref1o 16655 apdifflemr 16668 |
| Copyright terms: Public domain | W3C validator |