Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > addcl | Structured version Visualization version GIF version |
Description: Alias for ax-addcl 10675, for naming consistency with addcli 10725. Use this theorem instead of ax-addcl 10675 or axaddcl 10651. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 10675 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2114 (class class class)co 7170 ℂcc 10613 + caddc 10618 |
This theorem was proved from axioms: ax-addcl 10675 |
This theorem is referenced by: adddir 10710 0cn 10711 addcli 10725 addcld 10738 muladd11 10888 peano2cn 10890 muladd11r 10931 add4 10938 0cnALT2 10953 negeu 10954 pncan 10970 2addsub 10978 addsubeq4 10979 nppcan2 10995 pnpcan 11003 ppncan 11006 muladd 11150 mulsub 11161 recex 11350 muleqadd 11362 conjmul 11435 halfaddsubcl 11948 halfaddsub 11949 serf 13490 seradd 13504 sersub 13505 binom3 13677 bernneq 13682 lswccatn0lsw 14034 revccat 14217 2cshwcshw 14276 shftlem 14517 shftval2 14524 shftval5 14527 2shfti 14529 crre 14563 crim 14564 cjadd 14590 addcj 14597 sqabsadd 14732 absreimsq 14742 absreim 14743 abstri 14780 sqreulem 14809 sqreu 14810 addcn2 15041 o1add 15061 climadd 15079 clim2ser 15104 clim2ser2 15105 isermulc2 15107 isercolllem3 15116 summolem3 15164 summolem2a 15165 fsumcl 15183 fsummulc2 15232 fsumrelem 15255 binom 15278 isumsplit 15288 risefacval2 15456 risefaccl 15461 risefallfac 15470 risefacp1 15475 binomfallfac 15487 binomrisefac 15488 bpoly3 15504 efcj 15537 ef4p 15558 tanval3 15579 efi4p 15582 sinadd 15609 cosadd 15610 tanadd 15612 addsin 15615 demoivreALT 15646 opoe 15808 pythagtriplem4 16256 pythagtriplem12 16263 pythagtriplem14 16265 pythagtriplem16 16267 gzaddcl 16373 cnaddablx 19107 cnaddabl 19108 cncrng 20238 cnperf 23572 cnlmod 23892 cnstrcvs 23893 cncvs 23897 dvaddbr 24690 dvaddf 24694 dveflem 24731 plyaddcl 24969 plymulcl 24970 plysubcl 24971 coeaddlem 24998 dgrcolem1 25022 dgrcolem2 25023 quotlem 25048 quotcl2 25050 quotdgr 25051 sinperlem 25225 ptolemy 25241 tangtx 25250 sinkpi 25266 efif1olem2 25287 logrnaddcl 25318 logneg 25331 logimul 25357 cxpadd 25422 binom4 25588 atanf 25618 atanneg 25645 atancj 25648 efiatan 25650 atanlogaddlem 25651 atanlogadd 25652 atanlogsublem 25653 atanlogsub 25654 efiatan2 25655 2efiatan 25656 tanatan 25657 cosatan 25659 cosatanne0 25660 atantan 25661 atanbndlem 25663 atans2 25669 dvatan 25673 atantayl 25675 efrlim 25707 dfef2 25708 gamcvg2lem 25796 ftalem7 25816 prmorcht 25915 bposlem9 26028 lgsquad2lem1 26120 2sqlem2 26154 cncph 28754 hhssnv 29199 hoadddir 29739 superpos 30289 knoppcnlem8 34318 cos2h 35391 tan2h 35392 ftc1anclem3 35475 ftc1anclem7 35479 ftc1anclem8 35480 ftc1anc 35481 facp2 39705 fac2xp3 39751 fsumsermpt 42662 stirlinglem5 43161 stirlinglem7 43163 cnapbmcpd 44321 fmtnodvds 44530 opoeALTV 44669 mogoldbblem 44706 |
Copyright terms: Public domain | W3C validator |