Metamath Proof Explorer


Theorem abs2difabsi

Description: Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Hypotheses abs2difabsi.1 A
abs2difabsi.2 B
Assertion abs2difabsi A B A B

Proof

Step Hyp Ref Expression
1 abs2difabsi.1 A
2 abs2difabsi.2 B
3 abs2difabs A B A B A B
4 1 2 3 mp2an A B A B