This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A ≤ B
Assertion abssuble0d ⊢ φ → A − B = B − A

Proof

Step Hyp Ref Expression
1 absltd.1 ⊢ φ → A ∈ ℝ
2 absltd.2 ⊢ φ → B ∈ ℝ
3 abssubge0d.2 ⊢ φ → A ≤ B
4 abssuble0 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A − B = B − A
5 1 2 3 4 syl3anc ⊢ φ → A − B = B − A