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)