![]() |
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 7465 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 403 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 ax-addcl 7439 |
This theorem is referenced by: muladd11r 7636 negeu 7671 addsubass 7690 subsub2 7708 subsub4 7713 pnpcan 7719 pnncan 7721 addsub4 7723 pnpncand 7851 apreim 8078 addext 8085 divdirap 8162 recp1lt1 8358 cju 8419 cnref1o 9131 modsumfzodifsn 9799 ser3add 9931 expaddzap 9995 binom2 10061 binom3 10067 sqoddm1div8 10102 nn0opthlem1d 10124 reval 10279 imval 10280 crre 10287 remullem 10301 imval2 10324 cjreim2 10334 cnrecnv 10340 resqrexlemcalc1 10443 maxabslemab 10635 maxltsup 10647 max0addsup 10648 addcn2 10695 fsumadd 10796 isumadd 10821 binomlem 10873 efaddlem 10960 ef4p 10980 cosval 10990 cosf 10992 tanval2ap 11000 tanval3ap 11001 resin4p 11005 recos4p 11006 efival 11019 sinadd 11023 cosadd 11024 tanaddap 11026 oddennn 11479 qdencn 11870 |
Copyright terms: Public domain | W3C validator |