Metamath Proof Explorer


Theorem abs2difi

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

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

Proof

Step Hyp Ref Expression
1 abs2difi.1 A
2 abs2difi.2 B
3 abs2dif A B A B A B
4 1 2 3 mp2an A B A B