pnncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	pnncan	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B - (A - C) = B + C$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A \in ℂ$
2		simp2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to B \in ℂ$
3	1 2	addcld	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B \in ℂ$
4		simp3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to C \in ℂ$
5		subsub	$⊢ (A + B \in ℂ \land A \in ℂ \land C \in ℂ) \to A + B - (A - C) = (A + B) - A + C$
6	3 1 4 5	syl3anc	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B - (A - C) = (A + B) - A + C$
7		pncan2	$⊢ (A \in ℂ \land B \in ℂ) \to A + B - A = B$
8	7	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B - A = B$
9	8	oveq1d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A + B) - A + C = B + C$
10	6 9	eqtrd	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A + B - (A - C) = B + C$

Metamath Proof Explorer