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	$⊢ A \in ℂ$
	pncan3oi.2	$⊢ B \in ℂ$
Assertion	pncan3oi	$⊢ A + B - B = A$

Proof

Step	Hyp	Ref	Expression
1		pncan3oi.1	$⊢ A \in ℂ$
2		pncan3oi.2	$⊢ B \in ℂ$
3		pncan	$⊢ (A \in ℂ \land B \in ℂ) \to A + B - B = A$
4	1 2 3	mp2an	$⊢ A + B - B = A$