This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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