Metamath Proof Explorer

Theorem abssub

Description: Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abssub A B A B = B A


Step Hyp Ref Expression
1 subcl A B A B
2 absneg A B A B = A B
3 1 2 syl A B A B = A B
4 negsubdi2 A B A B = B A
5 4 fveq2d A B A B = B A
6 3 5 eqtr3d A B A B = B A