Theorem nnncan1

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

	Ref	Expression
Assertion	nnncan1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐶 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
2	1	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
3		sub32	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 − 𝐶 ) ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( ( 𝐴 − ( 𝐴 − 𝐶 ) ) − 𝐵 ) )
4	2 3	syld3an3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( ( 𝐴 − ( 𝐴 − 𝐶 ) ) − 𝐵 ) )
5		nncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐶 ) ) = 𝐶 )
6	5	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − ( 𝐴 − 𝐶 ) ) = 𝐶 )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − ( 𝐴 − 𝐶 ) ) − 𝐵 ) = ( 𝐶 − 𝐵 ) )
8	4 7	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) − ( 𝐴 − 𝐶 ) ) = ( 𝐶 − 𝐵 ) )