![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcl | Unicode version |
Description: Alias for ax-addcl 7938, for naming consistency with addcli 7992. Use this theorem instead of ax-addcl 7938 or axaddcl 7894. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7938 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-addcl 7938 |
This theorem is referenced by: adddir 7979 0cn 7980 addcli 7992 addcld 8008 muladd11 8121 peano2cn 8123 muladd11r 8144 add4 8149 cnegexlem3 8165 cnegex 8166 0cnALT 8178 negeu 8179 pncan 8194 2addsub 8202 addsubeq4 8203 nppcan2 8219 ppncan 8230 muladd 8372 mulsub 8389 recexap 8641 muleqadd 8656 conjmulap 8717 halfaddsubcl 9183 halfaddsub 9184 serf 10507 ser3add 10538 ser3sub 10539 ser0 10548 binom2 10666 binom3 10672 bernneq 10675 shftlem 10860 shftval2 10870 shftval5 10873 2shfti 10875 crre 10901 crim 10902 cjadd 10928 addcj 10935 sqabsadd 11099 absreimsq 11111 absreim 11112 abstri 11148 addcn2 11353 climadd 11369 clim2ser 11380 clim2ser2 11381 isermulc2 11383 serf0 11395 sumrbdclem 11420 fsum3cvg 11421 summodclem3 11423 summodclem2a 11424 zsumdc 11427 fsum3 11430 fsum3cvg2 11437 fsum3ser 11440 fsumcl2lem 11441 fsumcl 11443 sumsnf 11452 fsummulc2 11491 binom 11527 isumshft 11533 isumsplit 11534 geolim2 11555 cvgratnnlemseq 11569 cvgratz 11575 ef0lem 11703 efcj 11716 ef4p 11737 efgt1p 11739 tanval3ap 11757 efi4p 11760 sinadd 11779 cosadd 11780 tanaddap 11782 addsin 11785 demoivreALT 11816 opoe 11935 pythagtriplem4 12303 pythagtriplem12 12310 gzaddcl 12412 cncrng 13889 addccncf 14563 dvaddxxbr 14642 dvaddxx 14644 dviaddf 14646 dveflem 14664 sinperlem 14706 ptolemy 14722 tangtx 14736 sinkpi 14745 binom4 14874 2sqlem2 14940 |
Copyright terms: Public domain | W3C validator |