Theorem readdcl 11284

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  (class class class)co 7420  ℝcr 11200   + caddc 11204

This proof depends on axioms:  ax-addrcl 11262

This theorem is used by:  0re  11311  readdcli  11325  readdcld  11339  axltadd  11384  peano2re  11484  00id  11486  0cnALT  11546  resubcl  11623  ltaddsub  11791  leaddsub  11793  ltleadd  11800  ltaddsublt  11944  recex  11949  recp1lt1  12216  recreclt  12217  supadd  12286  cju  12317  nnge1  12367  addltmul  12583  avglt1  12585  avglt2  12586  avgle1  12587  avgle2  12588  nzadd  12745  irradd  13102  rpnnen1lem5  13110  rpaddcl  13145  xaddf  13355  xaddnemnf  13367  xaddnepnf  13368  xnegdi  13379  xaddass  13380  xadddilem  13425  iooshf  13558  ge0addcl  13592  icoshft  13605  icoshftf1o  13606  iccshftr  13618  difelfznle  13777  elfzodifsumelfzo  13867  subfzo0  13929  flbi2  13958  modcyc  14047  modadd1  14049  modsumfzodifsn  14088  serfre  14175  sermono  14178  serge0  14200  serle  14201  bernneq  14374  faclbnd6  14444  hashfun  14583  ccatsymb  14729  swrdswrdlem  14854  swrdccatin2  14879  cshweqrep  14973  cshwcsh2id  14980  readd  15294  imadd  15302  elicc4abs  15488  rddif  15509  absrdbnd  15510  caubnd2  15526  mulcn2  15764  o1add  15782  o1sub  15784  lo1add  15795  fsumrecl  15901  rerisefaccl  16185  rprisefaccl  16191  efgt1  16285  pythagtriplem12  17005  pythagtriplem14  17007  pythagtriplem16  17009  remulg  21914  resubdrg  21915  prdsxmetlem  24688  xmeter  24753  bl2ioo  25112  ioo2bl  25113  ioo2blex  25114  blssioo  25115  reperf  25140  reconnlem2  25148  opnreen  25152  icopnfcnv  25264  pcoass  25346  pjthlem1  25759  ovolun  25821  shft2rab  25830  volun  25867  mbfaddlem  25982  i1fadd  26017  itg1addlem4  26021  itg2monolem1  26072  ply1divex  26456  psercnlem1  26753  reefgim  26778  tangtx  26835  efif1olem1  26871  efif1olem2  26872  efif1o  26875  relogmul  26921  argimgt0  26941  logimul  26943  ang180lem1  27138  atanlogaddlem  27242  atanlogsublem  27244  atantan  27252  ressatans  27263  emcllem6  27329  basellem9  27417  ppiub  27532  bposlem5  27616  bposlem6  27617  bposlem9  27620  chpchtlim  27807  mulog2sumlem1  27862  mulog2sumlem2  27863  selberglem2  27874  pntrmax  27892  pntpbnd1a  27913  pntpbnd2  27915  pntibndlem3  27920  pntlemb  27925  pntlemk  27934  axsegconlem7  29502  axsegconlem9  29504  axsegconlem10  29505  clwwisshclwwslemlem  30605  eucrctshift  30845  pjhthlem1  31994  staddi  32849  stadd3i  32851  cdj1i  33036  cdj3lem2b  33040  cdj3i  33044  addltmulALT  33091  dp2cl  33489  rpdp2cl  33491  raddcn  34604  subfacval3  36023  dnicld1  37413  dnibndlem2  37420  dnibndlem3  37421  dnibndlem5  37423  dnibndlem7  37425  iooelexlt  38361  cos2h  38610  tan2h  38611  poimir  38647  heicant  38649  mblfinlem2  38652  mblfinlem3  38653  ismblfin  38655  ftc1anclem3  38689  ftc1anclem4  38690  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anclem8  38694  cntotbnd  38806  elre0re  43381  repncan2  43509  readdsub  43511  reltsubadd2  43514  resubsub4  43516  repnpcan  43519  reppncan  43520  pellexlem5  43916  ioomidp  46602  stoweidlem59  47145  stirlinglem10  47169  fourierdlem103  47295  fourierdlem104  47296  fouriersw  47317  sge0isum  47513  sge0seq  47532  hoidmvlelem2  47682  smflimlem4  47860  smfmullem1  47877  leaddsuble  48443  2leaddle2  48444  2elfz2melfz  48464  elfzelfzlble  48467  fmtnodvds  48705  gbegt5  48935  ltsubaddb  49702  ltsubadd2b  49704