Metamath Proof Explorer

Theorem lttri3

Description: Trichotomy law for 'less than'. (Contributed by NM, 5-May-1999)

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

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 sotrieq2 
 |-  ( ( < 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 ) ) )