Metamath Proof Explorer

Theorem maxle

Description: Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by NM, 29-Sep-2005)

Ref Expression
Assertion maxle ⊢ 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 xrmaxle ⊢ 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