Metamath Proof Explorer


Theorem pncan3s

Description: Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion pncan3s A No B No A + s B - s A = B

Proof

Step Hyp Ref Expression
1 eqid B - s A = B - s A
2 simpr A No B No B No
3 simpl A No B No A No
4 2 3 subscld A No B No B - s A No
5 2 3 4 subaddsd A No B No B - s A = B - s A A + s B - s A = B
6 1 5 mpbii A No B No A + s B - s A = B