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 AB¬A<BB<A

Proof

Step Hyp Ref Expression
1 ltso <Or
2 so2nr <OrAB¬A<BB<A
3 1 2 mpan AB¬A<BB<A