Metamath Proof Explorer

Theorem max1

Description: A number is less than or equal to the maximum of it and another. See also max1ALT . (Contributed by NM, 3-Apr-2005)

Ref Expression
Assertion max1 A B A if A B B A


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