![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > readdcl | Unicode version |
Description: Alias for ax-addrcl 7886, for naming consistency with readdcli 7948. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
readdcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addrcl 7886 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-addrcl 7886 |
This theorem is referenced by: 0re 7935 readdcli 7948 readdcld 7964 axltadd 8004 peano2re 8070 cnegexlem3 8111 cnegex 8112 resubcl 8198 ltleadd 8380 ltaddsublt 8505 recexap 8586 recreclt 8833 cju 8894 nnge1 8918 addltmul 9131 avglt1 9133 avglt2 9134 avgle1 9135 avgle2 9136 nzadd 9281 irradd 9622 rpaddcl 9651 xaddnemnf 9831 xaddnepnf 9832 xnegdi 9842 xaddass 9843 xltadd1 9850 iooshf 9926 ge0addcl 9955 icoshft 9964 icoshftf1o 9965 iccshftr 9968 difelfznle 10108 elfzodifsumelfzo 10174 subfzo0 10215 serfre 10448 ser3mono 10451 ser3ge0 10490 bernneq 10613 faclbnd6 10695 readd 10849 imadd 10857 elicc4abs 11074 caubnd2 11097 maxabsle 11184 maxabslemval 11188 maxcl 11190 mulcn2 11291 climserle 11324 fsumrecl 11380 mertenslem2 11515 ege2le3 11650 eftlub 11669 efgt1 11676 pythagtriplem12 12245 pythagtriplem14 12247 pythagtriplem16 12249 xmeter 13569 bl2ioo 13675 ioo2bl 13676 ioo2blex 13677 blssioo 13678 tangtx 13892 relogmul 13923 |
Copyright terms: Public domain | W3C validator |