Metamath Proof Explorer

Theorem maxlt

Description: Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007)

Ref Expression
Assertion maxlt ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → if A ≤ B B A < C ↔ A < C ∧ B < C

Proof

Step Hyp Ref Expression
1 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
2 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
3 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
4 xrmaxlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → if A ≤ B B A < C ↔ A < C ∧ B < C
5 1 2 3 4 syl3an ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → if A ≤ B B A < C ↔ A < C ∧ B < C