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 10585, for naming consistency with addcli 10635. Use this theorem instead of ax-addcl 10585 or axaddcl 10561. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcl 10585 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 |
This theorem was proved from axioms: ax-addcl 10585 |
This theorem is referenced by: adddir 10620 0cn 10621 addcli 10635 addcld 10648 muladd11 10798 peano2cn 10800 muladd11r 10841 add4 10848 0cnALT2 10863 negeu 10864 pncan 10880 2addsub 10888 addsubeq4 10889 nppcan2 10905 pnpcan 10913 ppncan 10916 muladd 11060 mulsub 11071 recex 11260 muleqadd 11272 conjmul 11345 halfaddsubcl 11857 halfaddsub 11858 serf 13386 seradd 13400 sersub 13401 binom3 13573 bernneq 13578 lswccatn0lsw 13933 revccat 14116 2cshwcshw 14175 shftlem 14415 shftval2 14422 shftval5 14425 2shfti 14427 crre 14461 crim 14462 cjadd 14488 addcj 14495 sqabsadd 14630 absreimsq 14640 absreim 14641 abstri 14678 sqreulem 14707 sqreu 14708 addcn2 14938 o1add 14958 climadd 14976 clim2ser 14999 clim2ser2 15000 isermulc2 15002 isercolllem3 15011 summolem3 15059 summolem2a 15060 fsumcl 15078 fsummulc2 15127 fsumrelem 15150 binom 15173 isumsplit 15183 risefacval2 15352 risefaccl 15357 risefallfac 15366 risefacp1 15371 binomfallfac 15383 binomrisefac 15384 bpoly3 15400 efcj 15433 ef4p 15454 tanval3 15475 efi4p 15478 sinadd 15505 cosadd 15506 tanadd 15508 addsin 15511 demoivreALT 15542 opoe 15700 pythagtriplem4 16144 pythagtriplem12 16151 pythagtriplem14 16153 pythagtriplem16 16155 gzaddcl 16261 cnaddablx 18917 cnaddabl 18918 cncrng 20494 cnperf 23355 cnlmod 23671 cnstrcvs 23672 cncvs 23676 dvaddbr 24462 dvaddf 24466 dveflem 24503 plyaddcl 24737 plymulcl 24738 plysubcl 24739 coeaddlem 24766 dgrcolem1 24790 dgrcolem2 24791 quotlem 24816 quotcl2 24818 quotdgr 24819 sinperlem 24993 ptolemy 25009 tangtx 25018 sinkpi 25034 efif1olem2 25054 logrnaddcl 25085 logneg 25098 logimul 25124 cxpadd 25189 binom4 25355 atanf 25385 atanneg 25412 atancj 25415 efiatan 25417 atanlogaddlem 25418 atanlogadd 25419 atanlogsublem 25420 atanlogsub 25421 efiatan2 25422 2efiatan 25423 tanatan 25424 cosatan 25426 cosatanne0 25427 atantan 25428 atanbndlem 25430 atans2 25436 dvatan 25440 atantayl 25442 efrlim 25474 dfef2 25475 gamcvg2lem 25563 ftalem7 25583 prmorcht 25682 bposlem9 25795 lgsquad2lem1 25887 2sqlem2 25921 cncph 28523 hhssnv 28968 hoadddir 29508 superpos 30058 knoppcnlem8 33736 cos2h 34764 tan2h 34765 ftc1anclem3 34850 ftc1anclem7 34854 ftc1anclem8 34855 ftc1anc 34856 fsumsermpt 41736 stirlinglem5 42240 stirlinglem7 42242 cnapbmcpd 43372 fmtnodvds 43583 opoeALTV 43725 mogoldbblem 43762 |
Copyright terms: Public domain | W3C validator |