| 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 11215, for naming consistency with addcli 11267. Use this theorem instead of ax-addcl 11215 or axaddcl 11191. (Contributed by NM, 10-Mar-2008.) |
| Ref | Expression |
|---|---|
| addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-addcl 11215 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 + caddc 11158 |
| This theorem was proved from axioms: ax-addcl 11215 |
| This theorem is referenced by: mpoaddf 11249 adddir 11252 0cn 11253 addcli 11267 addcld 11280 muladd11 11431 peano2cn 11433 muladd11r 11474 add4 11482 0cnALT2 11497 negeu 11498 pncan 11514 2addsub 11522 addsubeq4 11523 nppcan2 11540 pnpcan 11548 ppncan 11551 muladd 11695 mulsub 11706 recex 11895 muleqadd 11907 conjmul 11984 halfaddsubcl 12498 halfaddsub 12499 serf 14071 seradd 14085 sersub 14086 binom3 14263 bernneq 14268 lswccatn0lsw 14629 revccat 14804 2cshwcshw 14864 shftlem 15107 shftval2 15114 shftval5 15117 2shfti 15119 crre 15153 crim 15154 cjadd 15180 addcj 15187 sqabsadd 15321 absreimsq 15331 absreim 15332 abstri 15369 sqreulem 15398 sqreu 15399 addcn2 15630 o1add 15650 climadd 15668 clim2ser 15691 clim2ser2 15692 isermulc2 15694 isercolllem3 15703 summolem3 15750 summolem2a 15751 fsumcl 15769 fsummulc2 15820 fsumrelem 15843 binom 15866 isumsplit 15876 risefacval2 16046 risefaccl 16051 risefallfac 16060 risefacp1 16065 binomfallfac 16077 binomrisefac 16078 bpoly3 16094 efcj 16128 ef4p 16149 tanval3 16170 efi4p 16173 sinadd 16200 cosadd 16201 tanadd 16203 addsin 16206 demoivreALT 16237 opoe 16400 pythagtriplem4 16857 pythagtriplem12 16864 pythagtriplem14 16866 pythagtriplem16 16868 gzaddcl 16975 cnaddablx 19886 cnaddabl 19887 cncrng 21401 cncrngOLD 21402 cnperf 24842 cnlmod 25173 cnstrcvs 25174 cncvs 25178 dvaddbr 25974 dvaddf 25979 dveflem 26017 plyaddcl 26259 plymulcl 26260 plysubcl 26261 coeaddlem 26288 dgrcolem1 26313 dgrcolem2 26314 quotlem 26342 quotcl2 26344 quotdgr 26345 sinperlem 26522 ptolemy 26538 tangtx 26547 sinkpi 26564 efif1olem2 26585 logrnaddcl 26616 logneg 26630 logimul 26656 cxpadd 26721 binom4 26893 atanf 26923 atanneg 26950 atancj 26953 efiatan 26955 atanlogaddlem 26956 atanlogadd 26957 atanlogsublem 26958 atanlogsub 26959 efiatan2 26960 2efiatan 26961 tanatan 26962 cosatan 26964 cosatanne0 26965 atantan 26966 atanbndlem 26968 atans2 26974 dvatan 26978 atantayl 26980 efrlim 27012 efrlimOLD 27013 dfef2 27014 gamcvg2lem 27102 ftalem7 27122 prmorcht 27221 bposlem9 27336 lgsquad2lem1 27428 2sqlem2 27462 cncph 30838 hhssnv 31283 hoadddir 31823 superpos 32373 knoppcnlem8 36501 cos2h 37618 tan2h 37619 ftc1anclem3 37702 ftc1anclem7 37706 ftc1anclem8 37707 ftc1anc 37708 facp2 42144 fac2xp3 42240 sumcubes 42347 fsumsermpt 45594 stirlinglem5 46093 stirlinglem7 46095 cnapbmcpd 47307 fmtnodvds 47531 opoeALTV 47670 mogoldbblem 47707 |
| Copyright terms: Public domain | W3C validator |