Theorem pncan2

Description: Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005)

	Ref	Expression
Assertion	pncan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		addcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 ) )
2	1	oveq1d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 + 𝐴 ) − 𝐴 ) = ( ( 𝐴 + 𝐵 ) − 𝐴 ) )
3		pncan	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 + 𝐴 ) − 𝐴 ) = 𝐵 )
4	2 3	eqtr3d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )