Theorem readdcl 11099

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7355  ℝcr 11015   + caddc 11019

This theorem was proved from axioms:  ax-addrcl 11077

This theorem is referenced by:  0re  11124  readdcli  11137  readdcld  11151  axltadd  11196  peano2re  11296  00id  11298  0cnALT  11358  resubcl  11435  ltaddsub  11601  leaddsub  11603  ltleadd  11610  ltaddsublt  11754  recex  11759  recp1lt1  12030  recreclt  12031  supadd  12100  cju  12131  nnge1  12163  addltmul  12367  avglt1  12369  avglt2  12370  avgle1  12371  avgle2  12372  nzadd  12530  irradd  12881  rpnnen1lem5  12889  rpaddcl  12924  xaddf  13133  xaddnemnf  13145  xaddnepnf  13146  xnegdi  13157  xaddass  13158  xadddilem  13203  iooshf  13336  ge0addcl  13370  icoshft  13383  icoshftf1o  13384  iccshftr  13396  difelfznle  13552  elfzodifsumelfzo  13641  subfzo0  13702  flbi2  13731  modcyc  13820  modadd1  13822  modsumfzodifsn  13861  serfre  13948  sermono  13951  serge0  13973  serle  13974  bernneq  14146  faclbnd6  14216  hashfun  14354  ccatsymb  14500  swrdswrdlem  14621  swrdccatin2  14646  cshweqrep  14738  cshwcsh2id  14745  readd  15043  imadd  15051  elicc4abs  15237  rddif  15258  absrdbnd  15259  caubnd2  15275  mulcn2  15513  o1add  15531  o1sub  15533  lo1add  15544  fsumrecl  15651  rerisefaccl  15934  rprisefaccl  15940  efgt1  16035  pythagtriplem12  16748  pythagtriplem14  16750  pythagtriplem16  16752  remulg  21554  resubdrg  21555  prdsxmetlem  24293  xmeter  24358  bl2ioo  24717  ioo2bl  24718  ioo2blex  24719  blssioo  24720  reperf  24745  reconnlem2  24753  opnreen  24757  icopnfcnv  24877  pcoass  24961  pjthlem1  25374  ovolun  25437  shft2rab  25446  volun  25483  mbfaddlem  25598  i1fadd  25633  itg1addlem4  25637  itg2monolem1  25688  ply1divex  26079  psercnlem1  26372  reefgim  26397  tangtx  26451  efif1olem1  26488  efif1olem2  26489  efif1o  26492  relogmul  26538  argimgt0  26558  logimul  26560  ang180lem1  26756  atanlogaddlem  26860  atanlogsublem  26862  atantan  26870  ressatans  26881  emcllem6  26948  basellem9  27036  ppiub  27152  bposlem5  27236  bposlem6  27237  bposlem9  27240  chpchtlim  27427  mulog2sumlem1  27482  mulog2sumlem2  27483  selberglem2  27494  pntrmax  27512  pntpbnd1a  27533  pntpbnd2  27535  pntibndlem3  27540  pntlemb  27545  pntlemk  27554  axsegconlem7  28912  axsegconlem9  28914  axsegconlem10  28915  clwwisshclwwslemlem  30004  eucrctshift  30234  pjhthlem1  31382  staddi  32237  stadd3i  32239  cdj1i  32424  cdj3lem2b  32428  cdj3i  32432  addltmulALT  32437  dp2cl  32871  rpdp2cl  32873  raddcn  33953  subfacval3  35244  dnicld1  36527  dnibndlem2  36534  dnibndlem3  36535  dnibndlem5  36537  dnibndlem7  36539  iooelexlt  37417  cos2h  37661  tan2h  37662  poimir  37703  heicant  37705  mblfinlem2  37708  mblfinlem3  37709  ismblfin  37711  ftc1anclem3  37745  ftc1anclem4  37746  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  cntotbnd  37846  elre0re  42362  repncan2  42490  readdsub  42492  reltsubadd2  42495  resubsub4  42497  repnpcan  42500  reppncan  42501  pellexlem5  42940  ioomidp  45628  stoweidlem59  46171  stirlinglem10  46195  fourierdlem103  46321  fourierdlem104  46322  fouriersw  46343  sge0isum  46539  sge0seq  46558  hoidmvlelem2  46708  smflimlem4  46886  smfmullem1  46903  leaddsuble  47411  2leaddle2  47412  2elfz2melfz  47432  elfzelfzlble  47435  fmtnodvds  47658  gbegt5  47875  ltsubaddb  48629  ltsubadd2b  48631