Theorem readdcli 8346

Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
readdcli	⊢ (𝐴 + 𝐵) ∈ ℝ

Proof of Theorem readdcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		readdcl 8312	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 430	1 ⊢ (𝐴 + 𝐵) ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℝcr 8185   + caddc 8189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8283

This theorem is used by:  resubcli  8597  eqneg  9071  2re  9384  3re  9388  4re  9391  5re  9393  6re  9395  7re  9397  8re  9399  9re  9401  numltc  9819  ef01bndlem  12549  ballotfilem2  13287  log2ublog2  16236  bposlem8  16330  ex-fl  16956