Metamath Proof Explorer


Theorem readdcli

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

Ref Expression
Hypotheses recni.1 𝐴 ∈ ℝ
axri.2 𝐵 ∈ ℝ
Assertion readdcli ( 𝐴 + 𝐵 ) ∈ ℝ

Proof

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