Metamath Proof Explorer


Theorem min1

Description: The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007)

Ref Expression
Assertion min1 A B if A B A B A

Proof

Step Hyp Ref Expression
1 rexr A A *
2 rexr B B *
3 xrmin1 A * B * if A B A B A
4 1 2 3 syl2an A B if A B A B A