Theorem rexaddd

Description: The extended real addition operation when both arguments are real. Deduction version of rexadd . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	rexaddd.1	$$⊢\phi \to A\in ℝ$$
	rexaddd.2	$$⊢\phi \to B\in ℝ$$
Assertion	rexaddd	$$⊢\phi \to A{+}_{𝑒}B=A+B$$

Proof

Step	Hyp	Ref	Expression
1		rexaddd.1	$$⊢\phi \to A\in ℝ$$
2		rexaddd.2	$$⊢\phi \to B\in ℝ$$
3		rexadd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}B=A+B$$
4	1 2 3	syl2anc	$$⊢\phi \to A{+}_{𝑒}B=A+B$$