This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rexaddd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	rexaddd	⊢ ( 𝜑 → ( 𝐴 +_𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rexaddd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		rexaddd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +_𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝐴 +_𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )