Metamath Proof Explorer


Theorem max1d

Description: A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses max1d.1 ( 𝜑𝐴 ∈ ℝ )
max1d.2 ( 𝜑𝐵 ∈ ℝ )
Assertion max1d ( 𝜑𝐴 ≤ if ( 𝐴𝐵 , 𝐵 , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 max1d.1 ( 𝜑𝐴 ∈ ℝ )
2 max1d.2 ( 𝜑𝐵 ∈ ℝ )
3 max1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≤ if ( 𝐴𝐵 , 𝐵 , 𝐴 ) )
4 1 2 3 syl2anc ( 𝜑𝐴 ≤ if ( 𝐴𝐵 , 𝐵 , 𝐴 ) )