This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pnpcan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005) (Revised by Mario Carneiro, 27-May-2016) (Proof shortened by SN, 13-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2		subsub4	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) − 𝐴 ) − 𝐶 ) = ( ( 𝐴 + 𝐵 ) − ( 𝐴 + 𝐶 ) ) )
3	1 2	stoic4a	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) − 𝐴 ) − 𝐶 ) = ( ( 𝐴 + 𝐵 ) − ( 𝐴 + 𝐶 ) ) )
4		pncan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐴 ) = 𝐵 )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) − 𝐴 ) − 𝐶 ) = ( 𝐵 − 𝐶 ) )
7	3 6	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 + 𝐶 ) ) = ( 𝐵 − 𝐶 ) )