Theorem readdcl 11310

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7443  ℝcr 11226   + caddc 11230

This proof depends on axioms:  ax-addrcl 11288

This theorem is used by:  0re  11337  readdcli  11351  readdcld  11365  axltadd  11410  peano2re  11510  00id  11512  0cnALT  11572  resubcl  11649  ltaddsub  11817  leaddsub  11819  ltleadd  11826  ltaddsublt  11970  recex  11975  recp1lt1  12242  recreclt  12243  supadd  12312  cju  12343  nnge1  12393  addltmul  12609  avglt1  12611  avglt2  12612  avgle1  12613  avgle2  12614  nzadd  12771  irradd  13128  rpnnen1lem5  13136  rpaddcl  13171  xaddf  13381  xaddnemnf  13393  xaddnepnf  13394  xnegdi  13405  xaddass  13406  xadddilem  13451  iooshf  13584  ge0addcl  13618  icoshft  13631  icoshftf1o  13632  iccshftr  13644  difelfznle  13803  elfzodifsumelfzo  13893  subfzo0  13955  flbi2  13984  modcyc  14073  modadd1  14075  modsumfzodifsn  14114  serfre  14201  sermono  14204  serge0  14226  serle  14227  bernneq  14400  faclbnd6  14470  hashfun  14609  ccatsymb  14755  swrdswrdlem  14881  swrdccatin2  14906  cshweqrep  15000  cshwcsh2id  15007  readd  15322  imadd  15330  elicc4abs  15516  rddif  15537  absrdbnd  15538  caubnd2  15554  mulcn2  15792  o1add  15810  o1sub  15812  lo1add  15823  fsumrecl  15929  rerisefaccl  16213  rprisefaccl  16219  efgt1  16313  pythagtriplem12  17033  pythagtriplem14  17035  pythagtriplem16  17037  remulg  21943  resubdrg  21944  prdsxmetlem  24717  xmeter  24782  bl2ioo  25141  ioo2bl  25142  ioo2blex  25143  blssioo  25144  reperf  25169  reconnlem2  25177  opnreen  25181  icopnfcnv  25293  pcoass  25375  pjthlem1  25788  ovolun  25850  shft2rab  25859  volun  25896  mbfaddlem  26011  i1fadd  26046  itg1addlem4  26050  itg2monolem1  26101  ply1divex  26485  psercnlem1  26782  reefgim  26807  tangtx  26864  efif1olem1  26900  efif1olem2  26901  efif1o  26904  relogmul  26950  argimgt0  26970  logimul  26972  ang180lem1  27167  atanlogaddlem  27271  atanlogsublem  27273  atantan  27281  ressatans  27292  emcllem6  27358  basellem9  27446  ppiub  27561  bposlem5  27645  bposlem6  27646  bposlem9  27649  chpchtlim  27836  mulog2sumlem1  27891  mulog2sumlem2  27892  selberglem2  27903  pntrmax  27921  pntpbnd1a  27942  pntpbnd2  27944  pntibndlem3  27949  pntlemb  27954  pntlemk  27963  axsegconlem7  29531  axsegconlem9  29533  axsegconlem10  29534  clwwisshclwwslemlem  30634  eucrctshift  30874  pjhthlem1  32023  staddi  32878  stadd3i  32880  cdj1i  33065  cdj3lem2b  33069  cdj3i  33073  addltmulALT  33120  dp2cl  33516  rpdp2cl  33518  raddcn  34631  subfacval3  36121  dnicld1  37516  dnibndlem2  37523  dnibndlem3  37524  dnibndlem5  37526  dnibndlem7  37528  iooelexlt  38477  cos2h  38726  tan2h  38727  poimir  38763  heicant  38765  mblfinlem2  38768  mblfinlem3  38769  ismblfin  38771  ftc1anclem3  38805  ftc1anclem4  38806  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  cntotbnd  38922  elre0re  43498  repncan2  43626  readdsub  43628  reltsubadd2  43631  resubsub4  43633  repnpcan  43636  reppncan  43637  pellexlem5  44033  ioomidp  46731  stoweidlem59  47274  stirlinglem10  47298  fourierdlem103  47424  fourierdlem104  47425  fouriersw  47446  sge0isum  47642  sge0seq  47661  hoidmvlelem2  47811  smflimlem4  47989  smfmullem1  48006  leaddsuble  48572  2leaddle2  48573  2elfz2melfz  48593  elfzelfzlble  48596  fmtnodvds  48834  gbegt5  49064  ltsubaddb  49831  ltsubadd2b  49833