Theorem repnpcan

Description: Cancellation law for addition and real subtraction. Compare pnpcan . (Contributed by Steven Nguyen, 19-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		readdcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B\in ℝ$$
2		resubsub4	$$⊢\left(A+B\in ℝ\wedge A\in ℝ\wedge C\in ℝ\right)\to \left(\left(A+B\right){-}_{ℝ}A\right){-}_{ℝ}C=\left(A+B\right){-}_{ℝ}\left(A+C\right)$$
3	1 2	stoic4a	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(\left(A+B\right){-}_{ℝ}A\right){-}_{ℝ}C=\left(A+B\right){-}_{ℝ}\left(A+C\right)$$
4		repncan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A+B\right){-}_{ℝ}A=B$$
5	4	3adant3	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(A+B\right){-}_{ℝ}A=B$$
6	5	oveq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(\left(A+B\right){-}_{ℝ}A\right){-}_{ℝ}C=B{-}_{ℝ}C$$
7	3 6	eqtr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(A+B\right){-}_{ℝ}\left(A+C\right)=B{-}_{ℝ}C$$