Theorem readdcl 11210

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7416  ℝcr 11126   + caddc 11130

This proof depends on axioms:  ax-addrcl 11188

This theorem is used by:  0re  11237  readdcli  11251  readdcld  11265  axltadd  11310  peano2re  11410  00id  11412  0cnALT  11472  resubcl  11549  ltaddsub  11715  leaddsub  11717  ltleadd  11724  ltaddsublt  11868  recex  11873  recp1lt1  12140  recreclt  12141  supadd  12210  cju  12241  nnge1  12291  addltmul  12507  avglt1  12509  avglt2  12510  avgle1  12511  avgle2  12512  nzadd  12669  irradd  13025  rpnnen1lem5  13033  rpaddcl  13068  xaddf  13278  xaddnemnf  13290  xaddnepnf  13291  xnegdi  13302  xaddass  13303  xadddilem  13348  iooshf  13481  ge0addcl  13515  icoshft  13528  icoshftf1o  13529  iccshftr  13541  difelfznle  13699  elfzodifsumelfzo  13789  subfzo0  13851  flbi2  13880  modcyc  13969  modadd1  13971  modsumfzodifsn  14010  serfre  14097  sermono  14100  serge0  14122  serle  14123  bernneq  14295  faclbnd6  14365  hashfun  14504  ccatsymb  14650  swrdswrdlem  14775  swrdccatin2  14800  cshweqrep  14894  cshwcsh2id  14901  readd  15215  imadd  15223  elicc4abs  15409  rddif  15430  absrdbnd  15431  caubnd2  15447  mulcn2  15685  o1add  15703  o1sub  15705  lo1add  15716  fsumrecl  15822  rerisefaccl  16108  rprisefaccl  16114  efgt1  16208  pythagtriplem12  16922  pythagtriplem14  16924  pythagtriplem16  16926  remulg  21824  resubdrg  21825  prdsxmetlem  24598  xmeter  24663  bl2ioo  25022  ioo2bl  25023  ioo2blex  25024  blssioo  25025  reperf  25050  reconnlem2  25058  opnreen  25062  icopnfcnv  25174  pcoass  25256  pjthlem1  25669  ovolun  25731  shft2rab  25740  volun  25777  mbfaddlem  25892  i1fadd  25927  itg1addlem4  25931  itg2monolem1  25982  ply1divex  26367  psercnlem1  26661  reefgim  26686  tangtx  26743  efif1olem1  26780  efif1olem2  26781  efif1o  26784  relogmul  26830  argimgt0  26850  logimul  26852  ang180lem1  27047  atanlogaddlem  27151  atanlogsublem  27153  atantan  27161  ressatans  27172  emcllem6  27238  basellem9  27326  ppiub  27441  bposlem5  27525  bposlem6  27526  bposlem9  27529  chpchtlim  27716  mulog2sumlem1  27771  mulog2sumlem2  27772  selberglem2  27783  pntrmax  27801  pntpbnd1a  27822  pntpbnd2  27824  pntibndlem3  27829  pntlemb  27834  pntlemk  27843  axsegconlem7  29381  axsegconlem9  29383  axsegconlem10  29384  clwwisshclwwslemlem  30484  eucrctshift  30724  pjhthlem1  31873  staddi  32728  stadd3i  32730  cdj1i  32915  cdj3lem2b  32919  cdj3i  32923  addltmulALT  32928  dp2cl  33327  rpdp2cl  33329  raddcn  34441  subfacval3  35770  dnicld1  37171  dnibndlem2  37178  dnibndlem3  37179  dnibndlem5  37181  dnibndlem7  37183  iooelexlt  38118  cos2h  38367  tan2h  38368  poimir  38404  heicant  38406  mblfinlem2  38409  mblfinlem3  38410  ismblfin  38412  ftc1anclem3  38446  ftc1anclem4  38447  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anclem8  38451  cntotbnd  38548  elre0re  43123  repncan2  43259  readdsub  43261  reltsubadd2  43264  resubsub4  43266  repnpcan  43269  reppncan  43270  pellexlem5  43676  ioomidp  46346  stoweidlem59  46889  stirlinglem10  46913  fourierdlem103  47039  fourierdlem104  47040  fouriersw  47061  sge0isum  47257  sge0seq  47276  hoidmvlelem2  47426  smflimlem4  47604  smfmullem1  47621  leaddsuble  48187  2leaddle2  48188  2elfz2melfz  48208  elfzelfzlble  48211  fmtnodvds  48449  gbegt5  48679  ltsubaddb  49446  ltsubadd2b  49448