Metamath Proof Explorer


Theorem subeqrev

Description: Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013)

Ref Expression
Assertion subeqrev ABCDAB=CDBA=DC

Proof

Step Hyp Ref Expression
1 subcl ABAB
2 subcl CDCD
3 neg11 ABCDAB=CDAB=CD
4 1 2 3 syl2an ABCDAB=CDAB=CD
5 negsubdi2 ABAB=BA
6 negsubdi2 CDCD=DC
7 5 6 eqeqan12d ABCDAB=CDBA=DC
8 4 7 bitr3d ABCDAB=CDBA=DC