Metamath Proof Explorer

Theorem ltsub23

Description: 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999)

Ref Expression
Assertion ltsub23 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B<C↔A−C<B

Proof

Step Hyp Ref Expression
1 ltsubadd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A−B<C↔A<C+B
2 ltsubadd2 ⊢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