Metamath Proof Explorer

Theorem entri3

Description: Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of Mendelson p. 275. (Contributed by NM, 4-Jan-2004)

Ref Expression
Assertion entri3 A V B W A B B A


Step Hyp Ref Expression
1 entri2 A V B W A B B A
2 sdomdom B A B A
3 2 orim2i A B B A A B B A
4 1 3 syl A V B W A B B A