Metamath Proof Explorer

Theorem suble

Description: Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005)

Ref Expression
Assertion suble ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B≤C↔A−C≤B

Proof

Step Hyp Ref Expression
1 lesubadd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B≤C↔A≤C+B
2 lesubadd2 ⊢A∈ℝ∧C∈ℝ∧B∈ℝ→A−C≤B↔A≤C+B
3 2 3com23 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−C≤B↔A≤C+B
4 1 3 bitr4d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B≤C↔A−C≤B