![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addcl | Unicode version |
Description: Alias for ax-addcl 7740, for naming consistency with addcli 7794. Use this theorem instead of ax-addcl 7740 or axaddcl 7696. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 7740 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-addcl 7740 |
This theorem is referenced by: adddir 7781 0cn 7782 addcli 7794 addcld 7809 muladd11 7919 peano2cn 7921 muladd11r 7942 add4 7947 cnegexlem3 7963 cnegex 7964 0cnALT 7976 negeu 7977 pncan 7992 2addsub 8000 addsubeq4 8001 nppcan2 8017 ppncan 8028 muladd 8170 mulsub 8187 recexap 8438 muleqadd 8453 conjmulap 8513 halfaddsubcl 8977 halfaddsub 8978 serf 10278 ser3add 10309 ser3sub 10310 ser0 10318 binom2 10434 binom3 10440 bernneq 10443 shftlem 10620 shftval2 10630 shftval5 10633 2shfti 10635 crre 10661 crim 10662 cjadd 10688 addcj 10695 sqabsadd 10859 absreimsq 10871 absreim 10872 abstri 10908 addcn2 11111 climadd 11127 clim2ser 11138 clim2ser2 11139 isermulc2 11141 serf0 11153 sumrbdclem 11178 fsum3cvg 11179 summodclem3 11181 summodclem2a 11182 zsumdc 11185 fsum3 11188 fsum3cvg2 11195 fsum3ser 11198 fsumcl2lem 11199 fsumcl 11201 sumsnf 11210 fsummulc2 11249 binom 11285 isumshft 11291 isumsplit 11292 geolim2 11313 cvgratnnlemseq 11327 cvgratz 11333 ef0lem 11403 efcj 11416 ef4p 11437 efgt1p 11439 tanval3ap 11457 efi4p 11460 sinadd 11479 cosadd 11480 tanaddap 11482 addsin 11485 demoivreALT 11516 opoe 11628 addccncf 12794 dvaddxxbr 12873 dvaddxx 12875 dviaddf 12877 dveflem 12895 sinperlem 12937 ptolemy 12953 tangtx 12967 sinkpi 12976 |
Copyright terms: Public domain | W3C validator |