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 e. CC
	pncan3oi.2	|- B e. CC
Assertion	pncan3oi	|- ( ( A + B ) - B ) = A

Proof

Step	Hyp	Ref	Expression
1		pncan3oi.1	|- A e. CC
2		pncan3oi.2	|- B e. CC
3		pncan	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
4	1 2 3	mp2an	|- ( ( A + B ) - B ) = A