Metamath Proof Explorer


Theorem abssuble0d

Description: Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses absltd.1 φA
absltd.2 φB
abssubge0d.2 φAB
Assertion abssuble0d φAB=BA

Proof

Step Hyp Ref Expression
1 absltd.1 φA
2 absltd.2 φB
3 abssubge0d.2 φAB
4 abssuble0 ABABAB=BA
5 1 2 3 4 syl3anc φAB=BA