Metamath Proof Explorer

Theorem lttri2

Description: Consequence of trichotomy. (Contributed by NM, 9-Oct-1999)

Ref Expression
Assertion lttri2 
|- ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 sotrieq 
 |-  ( ( < Or RR /\ ( A e. RR /\ B e. RR ) ) -> ( A = B <-> -. ( A < B \/ B < A ) ) )
3 1 2 mpan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A = B <-> -. ( A < B \/ B < A ) ) )
4 3 bicomd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. ( A < B \/ B < A ) <-> A = B ) )
5 4 necon1abid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )