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

Metamath Proof Explorer

Theorem pncan3oi

Description: Subtraction and addition of equals. Almost but not exactly the same as pncan3i and pncan , this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand . (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	pncan3oi.1	⊢ 𝐴 ∈ ℂ
	pncan3oi.2	⊢ 𝐵 ∈ ℂ
Assertion	pncan3oi	⊢ ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		pncan3oi.1	⊢ 𝐴 ∈ ℂ
2		pncan3oi.2	⊢ 𝐵 ∈ ℂ
3		pncan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
4	1 2 3	mp2an	⊢ ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴