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