renpncan3

Description: Cancellation law for real subtraction. Compare npncan3 . (Contributed by Steven Nguyen, 28-Jan-2023)

		Ref	Expression
	Assertion	renpncan3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A -_{ℝ} B) + (C -_{ℝ} A) = C -_{ℝ} B$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A \in ℝ$
2		rersubcl	$⊢ (C \in ℝ \land A \in ℝ) \to C -_{ℝ} A \in ℝ$
3	2	ancoms	$⊢ (A \in ℝ \land C \in ℝ) \to C -_{ℝ} A \in ℝ$
4	3	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to C -_{ℝ} A \in ℝ$
5		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
6		readdsub	$⊢ (A \in ℝ \land C -_{ℝ} A \in ℝ \land B \in ℝ) \to (A + (C -_{ℝ} A)) -_{ℝ} B = (A -_{ℝ} B) + (C -_{ℝ} A)$
7	1 4 5 6	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A + (C -_{ℝ} A)) -_{ℝ} B = (A -_{ℝ} B) + (C -_{ℝ} A)$
8		repncan3	$⊢ (A \in ℝ \land C \in ℝ) \to A + (C -_{ℝ} A) = C$
9	8	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + (C -_{ℝ} A) = C$
10	9	oveq1d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A + (C -_{ℝ} A)) -_{ℝ} B = C -_{ℝ} B$
11	7 10	eqtr3d	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A -_{ℝ} B) + (C -_{ℝ} A) = C -_{ℝ} B$

Metamath Proof Explorer