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 7738 | . 2 | |
4 | 1, 2, 3 | syl2anc 408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 (class class class)co 5767 cc 7611 caddc 7616 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-addcl 7709 |
This theorem is referenced by: muladd11r 7911 negeu 7946 addsubass 7965 subsub2 7983 subsub4 7988 pnpcan 7994 pnncan 7996 addsub4 7998 pnpncand 8130 apreim 8358 addext 8365 aprcl 8401 divdirap 8450 recp1lt1 8650 cju 8712 cnref1o 9433 modsumfzodifsn 10162 expaddzap 10330 binom2 10396 binom3 10402 sqoddm1div8 10437 nn0opthlem1d 10459 reval 10614 imval 10615 crre 10622 remullem 10636 imval2 10659 cjreim2 10669 cnrecnv 10675 resqrexlemcalc1 10779 maxabslemab 10971 maxltsup 10983 max0addsup 10984 minabs 11000 bdtrilem 11003 bdtri 11004 addcn2 11072 fsumadd 11168 isumadd 11193 binomlem 11245 efaddlem 11369 ef4p 11389 cosval 11399 cosf 11401 tanval2ap 11409 tanval3ap 11410 resin4p 11414 recos4p 11415 efival 11428 sinadd 11432 cosadd 11433 tanaddap 11435 oddennn 11894 addccncf 12744 limcimolemlt 12791 dvaddxxbr 12823 ptolemy 12894 qdencn 13211 |
Copyright terms: Public domain | W3C validator |