![]() |
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 7528 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 404 |
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 107 ax-addcl 7502 |
This theorem is referenced by: muladd11r 7699 negeu 7734 addsubass 7753 subsub2 7771 subsub4 7776 pnpcan 7782 pnncan 7784 addsub4 7786 pnpncand 7914 apreim 8141 addext 8148 divdirap 8225 recp1lt1 8421 cju 8482 cnref1o 9194 modsumfzodifsn 9864 ser3add 9996 expaddzap 10060 binom2 10126 binom3 10132 sqoddm1div8 10167 nn0opthlem1d 10189 reval 10344 imval 10345 crre 10352 remullem 10366 imval2 10389 cjreim2 10399 cnrecnv 10405 resqrexlemcalc1 10508 maxabslemab 10700 maxltsup 10712 max0addsup 10713 addcn2 10760 fsumadd 10861 isumadd 10886 binomlem 10938 efaddlem 11025 ef4p 11045 cosval 11055 cosf 11057 tanval2ap 11065 tanval3ap 11066 resin4p 11070 recos4p 11071 efival 11084 sinadd 11088 cosadd 11089 tanaddap 11091 oddennn 11544 qdencn 12187 |
Copyright terms: Public domain | W3C validator |