Metamath Proof Explorer


Theorem somin2

Description: Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion somin2 R Or X A X B X if A R B A B R I B

Proof

Step Hyp Ref Expression
1 somincom R Or X A X B X if A R B A B = if B R A B A
2 somin1 R Or X B X A X if B R A B A R I B
3 2 ancom2s R Or X A X B X if B R A B A R I B
4 1 3 eqbrtrd R Or X A X B X if A R B A B R I B