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


Step Hyp Ref Expression
1 pncan3oi.1 A
2 pncan3oi.2 B
3 pncan A B A + B - B = A
4 1 2 3 mp2an A + B - B = A