Metamath Proof Explorer


Theorem lttri4

Description: Trichotomy law for 'less than'. (Contributed by NM, 20-Sep-2007) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion lttri4 A B A < B A = B B < A

Proof

Step Hyp Ref Expression
1 ltso < Or
2 solin < Or A B A < B A = B B < A
3 1 2 mpan A B A < B A = B B < A