Theorem readdcl 11110

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7358  ℝcr 11026   + caddc 11030

This theorem was proved from axioms:  ax-addrcl 11088

This theorem is referenced by:  0re  11135  readdcli  11149  readdcld  11163  axltadd  11208  peano2re  11308  00id  11310  0cnALT  11370  resubcl  11447  ltaddsub  11613  leaddsub  11615  ltleadd  11622  ltaddsublt  11766  recex  11771  recp1lt1  12043  recreclt  12044  supadd  12113  cju  12144  nnge1  12194  addltmul  12402  avglt1  12404  avglt2  12405  avgle1  12406  avgle2  12407  nzadd  12564  irradd  12912  rpnnen1lem5  12920  rpaddcl  12955  xaddf  13165  xaddnemnf  13177  xaddnepnf  13178  xnegdi  13189  xaddass  13190  xadddilem  13235  iooshf  13368  ge0addcl  13402  icoshft  13415  icoshftf1o  13416  iccshftr  13428  difelfznle  13585  elfzodifsumelfzo  13675  subfzo0  13736  flbi2  13765  modcyc  13854  modadd1  13856  modsumfzodifsn  13895  serfre  13982  sermono  13985  serge0  14007  serle  14008  bernneq  14180  faclbnd6  14250  hashfun  14388  ccatsymb  14534  swrdswrdlem  14655  swrdccatin2  14680  cshweqrep  14772  cshwcsh2id  14779  readd  15077  imadd  15085  elicc4abs  15271  rddif  15292  absrdbnd  15293  caubnd2  15309  mulcn2  15547  o1add  15565  o1sub  15567  lo1add  15578  fsumrecl  15685  rerisefaccl  15971  rprisefaccl  15977  efgt1  16072  pythagtriplem12  16786  pythagtriplem14  16788  pythagtriplem16  16790  remulg  21595  resubdrg  21596  prdsxmetlem  24342  xmeter  24407  bl2ioo  24766  ioo2bl  24767  ioo2blex  24768  blssioo  24769  reperf  24794  reconnlem2  24802  opnreen  24806  icopnfcnv  24918  pcoass  25000  pjthlem1  25413  ovolun  25475  shft2rab  25484  volun  25521  mbfaddlem  25636  i1fadd  25671  itg1addlem4  25675  itg2monolem1  25726  ply1divex  26114  psercnlem1  26406  reefgim  26431  tangtx  26485  efif1olem1  26522  efif1olem2  26523  efif1o  26526  relogmul  26572  argimgt0  26592  logimul  26594  ang180lem1  26790  atanlogaddlem  26894  atanlogsublem  26896  atantan  26904  ressatans  26915  emcllem6  26982  basellem9  27070  ppiub  27186  bposlem5  27270  bposlem6  27271  bposlem9  27274  chpchtlim  27461  mulog2sumlem1  27516  mulog2sumlem2  27517  selberglem2  27528  pntrmax  27546  pntpbnd1a  27567  pntpbnd2  27569  pntibndlem3  27574  pntlemb  27579  pntlemk  27588  axsegconlem7  29011  axsegconlem9  29013  axsegconlem10  29014  clwwisshclwwslemlem  30103  eucrctshift  30333  pjhthlem1  31482  staddi  32337  stadd3i  32339  cdj1i  32524  cdj3lem2b  32528  cdj3i  32532  addltmulALT  32537  dp2cl  32959  rpdp2cl  32961  raddcn  34094  subfacval3  35392  dnicld1  36745  dnibndlem2  36752  dnibndlem3  36753  dnibndlem5  36755  dnibndlem7  36757  iooelexlt  37689  cos2h  37943  tan2h  37944  poimir  37985  heicant  37987  mblfinlem2  37990  mblfinlem3  37991  ismblfin  37993  ftc1anclem3  38027  ftc1anclem4  38028  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  cntotbnd  38128  elre0re  42704  repncan2  42825  readdsub  42827  reltsubadd2  42830  resubsub4  42832  repnpcan  42835  reppncan  42836  pellexlem5  43276  ioomidp  45959  stoweidlem59  46502  stirlinglem10  46526  fourierdlem103  46652  fourierdlem104  46653  fouriersw  46674  sge0isum  46870  sge0seq  46889  hoidmvlelem2  47039  smflimlem4  47217  smfmullem1  47234  leaddsuble  47742  2leaddle2  47743  2elfz2melfz  47763  elfzelfzlble  47766  fmtnodvds  48004  gbegt5  48234  ltsubaddb  48987  ltsubadd2b  48989