Theorem repncan3

Description: Addition and subtraction of equals. Based on pncan3 . (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Assertion	repncan3	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(B{-}_{ℝ}A\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		rersubcl	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to B{-}_{ℝ}A\in ℝ$$
2		eqid	$$⊢B{-}_{ℝ}A=B{-}_{ℝ}A$$
3		resubadd	$$⊢\left(B\in ℝ\wedge A\in ℝ\wedge B{-}_{ℝ}A\in ℝ\right)\to \left(B{-}_{ℝ}A=B{-}_{ℝ}A\leftrightarrow A+\left(B{-}_{ℝ}A\right)=B\right)$$
4	2 3	mpbii	$$⊢\left(B\in ℝ\wedge A\in ℝ\wedge B{-}_{ℝ}A\in ℝ\right)\to A+\left(B{-}_{ℝ}A\right)=B$$
5	1 4	mpd3an3	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to A+\left(B{-}_{ℝ}A\right)=B$$
6	5	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\left(B{-}_{ℝ}A\right)=B$$