Theorem readdcl 9898

Description: Alias for ax-addrcl 9876, for naming consistency with readdcli 9932. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
readdcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 9876	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814   + caddc 9818

This theorem was proved from axioms:  ax-addrcl 9876

This theorem is referenced by:  0re  9919  readdcli  9932  readdcld  9948  axltadd  9990  peano2re  10088  00id  10090  resubcl  10224  ltaddsub  10381  leaddsub  10383  ltleadd  10390  ltaddsublt  10533  recex  10538  recp1lt1  10800  recreclt  10801  supadd  10868  cju  10893  nnge1  10923  addltmul  11145  avglt1  11147  avglt2  11148  avgle1  11149  avgle2  11150  nzadd  11302  irradd  11688  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  rpaddcl  11730  xaddf  11929  xaddnemnf  11941  xaddnepnf  11942  xnegdi  11950  xaddass  11951  xadddilem  11996  iooshf  12123  ge0addcl  12155  icoshft  12165  icoshftf1o  12166  iccshftr  12177  difelfznle  12322  elfzodifsumelfzo  12401  subfzo0  12452  flbi2  12480  modcyc  12567  modadd1  12569  modsumfzodifsn  12605  serfre  12692  sermono  12695  serge0  12717  serle  12718  bernneq  12852  faclbnd6  12948  hashfun  13084  ccatsymb  13219  swrdswrdlem  13311  swrdccatin2  13338  cshweqrep  13418  cshwcsh2id  13425  readd  13714  imadd  13722  elicc4abs  13907  rddif  13928  absrdbnd  13929  caubnd2  13945  mulcn2  14174  o1add  14192  o1sub  14194  lo1add  14205  fsumrecl  14312  rerisefaccl  14587  rprisefaccl  14593  efgt1  14685  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  remulg  19772  resubdrg  19773  prdsxmetlem  21983  xmeter  22048  bl2ioo  22403  ioo2bl  22404  ioo2blex  22405  blssioo  22406  reperf  22430  reconnlem2  22438  opnreen  22442  icopnfcnv  22549  pcoass  22632  pjthlem1  23016  ovolun  23074  shft2rab  23083  volun  23120  mbfaddlem  23233  i1fadd  23268  itg1addlem4  23272  itg2monolem1  23323  ply1divex  23700  psercnlem1  23983  reefgim  24008  tangtx  24061  efif1olem1  24092  efif1olem2  24093  efif1o  24096  relogmul  24142  argimgt0  24162  logimul  24164  ang180lem1  24339  atanlogaddlem  24440  atanlogsublem  24442  atantan  24450  ressatans  24461  emcllem6  24527  basellem9  24615  ppiub  24729  bposlem5  24813  bposlem6  24814  bposlem9  24817  chpchtlim  24968  mulog2sumlem1  25023  mulog2sumlem2  25024  selberglem2  25035  pntrmax  25053  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem3  25081  pntlemb  25086  pntlemk  25095  axsegconlem7  25603  axsegconlem9  25605  axsegconlem10  25606  clwwisshclwwlem1  26333  pjhthlem1  27634  staddi  28489  stadd3i  28491  cdj1i  28676  cdj3lem2b  28680  cdj3i  28684  addltmulALT  28689  raddcn  29303  subfacval3  30425  dnicld1  31632  dnibndlem2  31639  dnibndlem3  31640  dnibndlem5  31642  dnibndlem7  31644  iooelexlt  32386  cos2h  32570  tan2h  32571  poimir  32612  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  cntotbnd  32765  pellexlem5  36415  ioomidp  38587  stoweidlem59  38952  stirlinglem10  38976  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  sge0isum  39320  sge0seq  39339  hoidmvlelem2  39486  smflimlem4  39660  smfmullem1  39676  fmtnodvds  39994  gbegt5  40183  leaddsuble  40343  2leaddle2  40344  2elfz2melfz  40355  elfzelfzlble  40358  clwwisshclwwslemlem  41233  eucrctshift  41411  ltsubaddb  42098  ltsubadd2b  42100  dp2cl  42309