Metamath Proof Explorer


Theorem entri2

Description: Trichotomy of dominance and strict dominance. (Contributed by NM, 4-Jan-2004)

Ref Expression
Assertion entri2 AVBWABBA

Proof

Step Hyp Ref Expression
1 entric AVBWABABBA
2 brdom2 ABABAB
3 2 orbi1i ABBAABABBA
4 df-3or ABABBAABABBA
5 3 4 bitr4i ABBAABABBA
6 1 5 sylibr AVBWABBA