Theorem readdid2

Description: Real number version of addid2 . (Contributed by SN, 23-Jan-2024)

	Ref	Expression
Assertion	readdid2	$$⊢A\in ℝ\to 0+A=A$$

Proof

Step	Hyp	Ref	Expression
1		re0m0e0	$$⊢0{-}_{ℝ}0=0$$
2	1	oveq1i	$$⊢\left(0{-}_{ℝ}0\right)+A=0+A$$
3		reneg0addid2	$$⊢A\in ℝ\to \left(0{-}_{ℝ}0\right)+A=A$$
4	2 3	syl5eqr	$$⊢A\in ℝ\to 0+A=A$$