Theorem readdcl 11189

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  (class class class)co 7412  ℝcr 11105   + caddc 11109

This proof depends on axioms:  ax-addrcl 11167

This theorem is used by:  0re  11216  readdcli  11230  readdcld  11244  axltadd  11289  peano2re  11389  00id  11391  0cnALT  11451  resubcl  11528  ltaddsub  11694  leaddsub  11696  ltleadd  11703  ltaddsublt  11847  recex  11852  recp1lt1  12119  recreclt  12120  supadd  12189  cju  12220  nnge1  12270  addltmul  12486  avglt1  12488  avglt2  12489  avgle1  12490  avgle2  12491  nzadd  12648  irradd  13003  rpnnen1lem5  13011  rpaddcl  13046  xaddf  13256  xaddnemnf  13268  xaddnepnf  13269  xnegdi  13280  xaddass  13281  xadddilem  13326  iooshf  13459  ge0addcl  13493  icoshft  13506  icoshftf1o  13507  iccshftr  13519  difelfznle  13677  elfzodifsumelfzo  13767  subfzo0  13828  flbi2  13857  modcyc  13946  modadd1  13948  modsumfzodifsn  13987  serfre  14074  sermono  14077  serge0  14099  serle  14100  bernneq  14272  faclbnd6  14342  hashfun  14481  ccatsymb  14627  swrdswrdlem  14748  swrdccatin2  14773  cshweqrep  14865  cshwcsh2id  14872  readd  15184  imadd  15192  elicc4abs  15378  rddif  15399  absrdbnd  15400  caubnd2  15416  mulcn2  15654  o1add  15672  o1sub  15674  lo1add  15685  fsumrecl  15792  rerisefaccl  16078  rprisefaccl  16084  efgt1  16178  pythagtriplem12  16892  pythagtriplem14  16894  pythagtriplem16  16896  remulg  21768  resubdrg  21769  prdsxmetlem  24536  xmeter  24601  bl2ioo  24960  ioo2bl  24961  ioo2blex  24962  blssioo  24963  reperf  24988  reconnlem2  24996  opnreen  25000  icopnfcnv  25112  pcoass  25194  pjthlem1  25607  ovolun  25669  shft2rab  25678  volun  25715  mbfaddlem  25830  i1fadd  25865  itg1addlem4  25869  itg2monolem1  25920  ply1divex  26305  psercnlem1  26599  reefgim  26624  tangtx  26681  efif1olem1  26718  efif1olem2  26719  efif1o  26722  relogmul  26768  argimgt0  26788  logimul  26790  ang180lem1  26985  atanlogaddlem  27089  atanlogsublem  27091  atantan  27099  ressatans  27110  emcllem6  27176  basellem9  27264  ppiub  27379  bposlem5  27463  bposlem6  27464  bposlem9  27467  chpchtlim  27654  mulog2sumlem1  27709  mulog2sumlem2  27710  selberglem2  27721  pntrmax  27739  pntpbnd1a  27760  pntpbnd2  27762  pntibndlem3  27767  pntlemb  27772  pntlemk  27781  axsegconlem7  29284  axsegconlem9  29286  axsegconlem10  29287  clwwisshclwwslemlem  30375  eucrctshift  30605  pjhthlem1  31754  staddi  32609  stadd3i  32611  cdj1i  32796  cdj3lem2b  32800  cdj3i  32804  addltmulALT  32809  dp2cl  33210  rpdp2cl  33212  raddcn  34328  subfacval3  35689  dnicld1  37089  dnibndlem2  37096  dnibndlem3  37097  dnibndlem5  37099  dnibndlem7  37101  iooelexlt  38036  cos2h  38290  tan2h  38291  poimir  38332  heicant  38334  mblfinlem2  38337  mblfinlem3  38338  ismblfin  38340  ftc1anclem3  38374  ftc1anclem4  38375  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  cntotbnd  38475  elre0re  43050  repncan2  43171  readdsub  43173  reltsubadd2  43176  resubsub4  43178  repnpcan  43181  reppncan  43182  pellexlem5  43588  ioomidp  46258  stoweidlem59  46801  stirlinglem10  46825  fourierdlem103  46951  fourierdlem104  46952  fouriersw  46973  sge0isum  47169  sge0seq  47188  hoidmvlelem2  47338  smflimlem4  47516  smfmullem1  47533  leaddsuble  48062  2leaddle2  48063  2elfz2melfz  48083  elfzelfzlble  48086  fmtnodvds  48324  gbegt5  48554  ltsubaddb  49322  ltsubadd2b  49324