Theorem readdcl 10963

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  (class class class)co 7284  ℝcr 10879   + caddc 10883

This theorem was proved from axioms:  ax-addrcl 10941

This theorem is referenced by:  0re  10986  readdcli  10999  readdcld  11013  axltadd  11057  peano2re  11157  00id  11159  0cnALT  11218  resubcl  11294  ltaddsub  11458  leaddsub  11460  ltleadd  11467  ltaddsublt  11611  recex  11616  recp1lt1  11882  recreclt  11883  supadd  11952  cju  11978  nnge1  12010  addltmul  12218  avglt1  12220  avglt2  12221  avgle1  12222  avgle2  12223  nzadd  12377  irradd  12722  rpnnen1lem5  12730  rpaddcl  12761  xaddf  12967  xaddnemnf  12979  xaddnepnf  12980  xnegdi  12991  xaddass  12992  xadddilem  13037  iooshf  13167  ge0addcl  13201  icoshft  13214  icoshftf1o  13215  iccshftr  13227  difelfznle  13379  elfzodifsumelfzo  13462  subfzo0  13518  flbi2  13546  modcyc  13635  modadd1  13637  modsumfzodifsn  13673  serfre  13761  sermono  13764  serge0  13786  serle  13787  bernneq  13953  faclbnd6  14022  hashfun  14161  ccatsymb  14296  swrdswrdlem  14426  swrdccatin2  14451  cshweqrep  14543  cshwcsh2id  14550  readd  14846  imadd  14854  elicc4abs  15040  rddif  15061  absrdbnd  15062  caubnd2  15078  mulcn2  15314  o1add  15332  o1sub  15334  lo1add  15345  fsumrecl  15455  rerisefaccl  15736  rprisefaccl  15742  efgt1  15834  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem16  16540  remulg  20821  resubdrg  20822  prdsxmetlem  23530  xmeter  23595  bl2ioo  23964  ioo2bl  23965  ioo2blex  23966  blssioo  23967  reperf  23991  reconnlem2  23999  opnreen  24003  icopnfcnv  24114  pcoass  24196  pjthlem1  24610  ovolun  24672  shft2rab  24681  volun  24718  mbfaddlem  24833  i1fadd  24868  itg1addlem4  24872  itg1addlem4OLD  24873  itg2monolem1  24924  ply1divex  25310  psercnlem1  25593  reefgim  25618  tangtx  25671  efif1olem1  25707  efif1olem2  25708  efif1o  25711  relogmul  25756  argimgt0  25776  logimul  25778  ang180lem1  25968  atanlogaddlem  26072  atanlogsublem  26074  atantan  26082  ressatans  26093  emcllem6  26159  basellem9  26247  ppiub  26361  bposlem5  26445  bposlem6  26446  bposlem9  26449  chpchtlim  26636  mulog2sumlem1  26691  mulog2sumlem2  26692  selberglem2  26703  pntrmax  26721  pntpbnd1a  26742  pntpbnd2  26744  pntibndlem3  26749  pntlemb  26754  pntlemk  26763  axsegconlem7  27300  axsegconlem9  27302  axsegconlem10  27303  clwwisshclwwslemlem  28386  eucrctshift  28616  pjhthlem1  29762  staddi  30617  stadd3i  30619  cdj1i  30804  cdj3lem2b  30808  cdj3i  30812  addltmulALT  30817  dp2cl  31163  rpdp2cl  31165  raddcn  31888  subfacval3  33160  dnicld1  34661  dnibndlem2  34668  dnibndlem3  34669  dnibndlem5  34671  dnibndlem7  34673  iooelexlt  35542  cos2h  35777  tan2h  35778  poimir  35819  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  cntotbnd  35963  2xp3dxp2ge1d  40169  elre0re  40298  repncan2  40372  readdsub  40374  reltsubadd2  40377  resubsub4  40379  repnpcan  40382  reppncan  40383  pellexlem5  40662  ioomidp  43059  stoweidlem59  43607  stirlinglem10  43631  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  sge0isum  43972  sge0seq  43991  hoidmvlelem2  44141  smflimlem4  44319  smfmullem1  44336  leaddsuble  44800  2leaddle2  44801  2elfz2melfz  44821  elfzelfzlble  44824  fmtnodvds  45007  gbegt5  45224  ltsubaddb  45866  ltsubadd2b  45868