Metamath Proof Explorer

Theorem ltnsym2

Description: 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 so2nr 
 |-  ( ( < Or RR /\ ( A e. RR /\ B e. RR ) ) -> -. ( A < B /\ B < A ) )
3 1 2 mpan 
 |-  ( ( A e. RR /\ B e. RR ) -> -. ( A < B /\ B < A ) )