Metamath Proof Explorer


Theorem sotrieq2

Description: Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999)

Ref Expression
Assertion sotrieq2 R Or A B A C A B = C ¬ B R C ¬ C R B

Proof

Step Hyp Ref Expression
1 sotrieq R Or A B A C A B = C ¬ B R C C R B
2 ioran ¬ B R C C R B ¬ B R C ¬ C R B
3 1 2 bitrdi R Or A B A C A B = C ¬ B R C ¬ C R B