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 7713 | . 2 | |
4 | 1, 2, 3 | syl2anc 408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 (class class class)co 5742 cc 7586 caddc 7591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-addcl 7684 |
This theorem is referenced by: muladd11r 7886 negeu 7921 addsubass 7940 subsub2 7958 subsub4 7963 pnpcan 7969 pnncan 7971 addsub4 7973 pnpncand 8105 apreim 8333 addext 8340 aprcl 8376 divdirap 8425 recp1lt1 8625 cju 8687 cnref1o 9408 modsumfzodifsn 10137 expaddzap 10305 binom2 10371 binom3 10377 sqoddm1div8 10412 nn0opthlem1d 10434 reval 10589 imval 10590 crre 10597 remullem 10611 imval2 10634 cjreim2 10644 cnrecnv 10650 resqrexlemcalc1 10754 maxabslemab 10946 maxltsup 10958 max0addsup 10959 minabs 10975 bdtrilem 10978 bdtri 10979 addcn2 11047 fsumadd 11143 isumadd 11168 binomlem 11220 efaddlem 11307 ef4p 11327 cosval 11337 cosf 11339 tanval2ap 11347 tanval3ap 11348 resin4p 11352 recos4p 11353 efival 11366 sinadd 11370 cosadd 11371 tanaddap 11373 oddennn 11832 addccncf 12682 limcimolemlt 12729 dvaddxxbr 12761 ptolemy 12832 qdencn 13149 |
Copyright terms: Public domain | W3C validator |