![]() |
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 7769 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 409 |
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 107 ax-addcl 7740 |
This theorem is referenced by: muladd11r 7942 negeu 7977 addsubass 7996 subsub2 8014 subsub4 8019 pnpcan 8025 pnncan 8027 addsub4 8029 pnpncand 8161 apreim 8389 addext 8396 aprcl 8432 divdirap 8481 recp1lt1 8681 cju 8743 cnref1o 9469 modsumfzodifsn 10200 expaddzap 10368 binom2 10434 binom3 10440 sqoddm1div8 10475 nn0opthlem1d 10498 reval 10653 imval 10654 crre 10661 remullem 10675 imval2 10698 cjreim2 10708 cnrecnv 10714 resqrexlemcalc1 10818 maxabslemab 11010 maxltsup 11022 max0addsup 11023 minabs 11039 bdtrilem 11042 bdtri 11043 addcn2 11111 fsumadd 11207 isumadd 11232 binomlem 11284 efaddlem 11417 ef4p 11437 cosval 11446 cosf 11448 tanval2ap 11456 tanval3ap 11457 resin4p 11461 recos4p 11462 efival 11475 sinadd 11479 cosadd 11480 tanaddap 11482 oddennn 11941 addccncf 12794 limcimolemlt 12841 dvaddxxbr 12873 ptolemy 12953 rpcxpadd 13034 qdencn 13397 apdifflemr 13415 iooref1o 13426 |
Copyright terms: Public domain | W3C validator |